Ping

[Francis Southern]

Dear typists,

Exams are now certainly over; what's the plan?

I'd like to resume regular meetings doing something, I don't really mind
what, just because it would give my life some kind of structure now that
I've got nothing to do other than despair^H^H^H^H^H^H^H work on my
dissertation. The same Tuesday afternoon would be good for me.

In other news, I've been offered a place at the CDT, so long as I get a
distinction. Which I've been told I should get, in theory...

Anyway, I look forward to meeting up with you soon,
Francis

[geln...@cs.man.ac.uk]

I am, unfortunately moved back down south, and have secured employment in
London. Therefore I shall, unfortunately not be around for future
sessions.

It has been fun, and a pleasure to have met you all.

[Yegor Guskov]

I can attend regular meetings during summer any day after 17:00, which
would be even better than during the other time of the year, as there
is more time to read the book.

[Joseph Razavi]

Any day after 17:00 should suit me too.

[Salman Aljammaz]

Joseph Razavi <jabr...@gmail.com> wrote:
> Any day after 17:00 should suit me too.

me too.

p.s. hi everyone.

[Giles Reger]

Today being Tuesday, we could meet at 17.00 today to discuss how we wish to proceed (and for general banter, which I miss)

p.s. hello

[regerg]

How about meeting tomorrow (Tuesday) at 17.00 to discuss how we wish to

proceed (and for general banter, which I miss)

On Mon, 11 Jun 2012 18:48:04 +0100, Joseph Razavi <jabr...@gmail.com>
wrote:

[reg...@cs.man.ac.uk]

Congratulations on getting onto the CDT. A distinction in theory sounds good ;)

I'm up for continued meetings, I think there was some talk about developing material for next year.

Giles

Sent from my HTC

[Joseph Razavi]

Sorry I didn't show up today, I didn't read my email in time -- and
some of Giles' were held as spam!

[Francis Southern]

Did anyone show up yesterday? My excuse is that I was in Surrey
visiting Royal Holloway's type theory group, which was a lot of fun!

I'd be up for meeting today and then resuming normal Tuesday service
next week, if anyone else thought that was a good idea.

Francis

(Obligatory: In theory, distinctions in theory are as good as in
practice, but in practice this isn't always the case.)

[regerg]

> Did anyone show up yesterday?

I have to admit, even as the one suggesting the meeting, I did not show up
either. I was planning on going down and seeing if anybody turned up but I
got distracted.

> My excuse is that I was in Surrey visiting Royal Holloway's type theory
group, which was a lot of fun!

That does sound like a lot of fun - you'll have to report back to us.

> I'd be up for meeting today and then resuming normal Tuesday service
> next week, if anyone else thought that was a good idea.

I'm not in Manchester today but am on Friday and then I'm undecided on
next week.

[Joseph Razavi]

I'll now be out of town until around Thursday next week. Let me know
how your meeting(s) in that time go ;)

Joe

[Joseph Razavi]

Hi All,

I'm assuming no meeting today; if not and you see this message in time
let me know and I'll pop in. What do people think of meeting next
week?

Joe

[Giles Reger]

Hi Joe,

Meeting next week sounds like a fantastic idea, and I will definitely turn up!

I can do any time any day except Monday and Friday... or do we want to stick to our standard Tuesday slot?

Giles

*************************
Giles Reger
giles...@cs.man.ac.uk
gre...@cantab.net
07939 486 756
*************************

[Jonas Lorenz]

Hi Everyone,

I am generally interested and generally around. This is true for this
week, next week and most other weeks except for three in the middle of
August.
So if anyone announces on this mailing list (at least 15 minutes
before the time) that they will show up, then I will try to show up
too.

See you all soon,
Jonas

[Francis Southern]

Hi,

I can basically make it any time too (although yesterday I was watching
Richard Stallman's talk) and I'd definitely be happy with next Tuesday
at five.

Francis

[Yegor Guskov]

Has there been a meeting this week?

I have not found anybody around the usual place at 17:03.

By the way, that room is not suitable for meetings anymore due to some
renovation works at that part of the building, if you have not found
that out yet.

Yegor Guskov

[Joseph Razavi]

Hi,

Sorry Yegor (and anybody else who tried to find me); I bumped into
some evangelical Christians just outside Kilburn and didn't realise
that I talked to them for some time!

If anybody wants to talk types today, I'll be in the 3rd Year Lab
until 6.00pm -- or let me know if you've gone somewhere else.

Otherwise, the agenda as I see it this summer is to try to find
reading for the following topics:

1) Intuitionistic Propositional Logic
2) The (untyped) lambda calculus
3) The simply typed lambda calculus (or just the "theory of simple types")
4) The Curry-Howard isomorphism
5) The curry-howard isomorphism for other logics (eps. first order)

I think we should aim to cover 1-4 in the first semester, but the
point of saying all this is to invite comments! My imagined session
style is that we do the reading *in session* together (while asking
people to read ahead of time if possible) -- that way we might
actually get people to read something :P

Joe

[Francis Southern]

Oops, sorry, I completely forgot about this. Working on my dissertation
is consuming a lot more of my brain than I thought it would and I still
don't feel like I'm getting very far!

Still, I'll really try and be there next week and maybe even with
something useful to say.

Francis

[Giles Reger]

Yegor,

To quote my previous email

"Meeting next week sounds like a fantastic idea, and I will definitely turn up!"

Oh dear.

Sorry I wasn't there - I failed to put it in my calendar, so when I failed to catch my normal train I decided it wasn't worth coming into Manchester.

Note to self : Must try harder.

Francis,

Working on my dissertation is consuming a lot more of my brain than I thought it would and I still don't feel like I'm getting very far!

That always seems the way! Personally, I suffer from chronic over-ambition, which can cause headaches, tiredness and, occasionally, howling at the moon. Insert comment about only seeing your path from the top of the mountain or something.

 

Joe,

 

Otherwise, the agenda as I see it this summer is to try to find
reading for the following topics:

1) Intuitionistic Propositional Logic
2) The (untyped) lambda calculus
3) The simply typed lambda calculus (or just the "theory of simple types")
4) The Curry-Howard isomorphism
5) The curry-howard isomorphism for other logics (eps. first order)

I think we should aim to cover 1-4 in the first semester, but the
point of saying all this is to invite comments! My imagined session
style is that we do the reading *in session* together (while asking
people to read ahead of time if possible) -- that way we might
actually get people to read something :P

Sounds like a wonderful plan, and a good order. Are we also planning on looking at Coq in some form - I'm very excited about the prospect of Coq.

An alternative session style would be to take it in turns to do the reading and then present it back to the group, followed by some discussion. This format would mean we get through more material but would also require more work, but it would be less frequent then last year's format. To encourage newcomers we could draw volunteers to do the reading/presenting from us oldies.

Giles

[Joseph Razavi]

Hi all (and Giles in particular),

> Are we also planning on looking at Coq in some form - I'm very excited about the prospect > of Coq.

Indeed, my mind is constantly occupied by thoughts about Coq. One
advantage of putting IPL first is that it means we could start Coq

[Joseph Razavi]

Hi everyone (especially Giels) again,

It seems gmail has a keyboard shortcut to "send" which I didn't know
about! sorry for the repeated email. Nevertheless:

> Are we also planning on looking at Coq in some form - I'm very excited about the prospect > of Coq.

I'm always thinking of Coq. One advantage of putting IPL first is that
we couls start coq labs right away on a natural (and well-covered...
for Coq) topic.

> An alternative session style would be to take it in turns to do the reading
> and then present it back to the group, followed by some discussion. This
> format would mean we get through more material but would also require more
> work, but it would be less frequent then last year's format. To encourage
> newcomers we could draw volunteers to do the reading/presenting from us
> oldies.

That's an interesting thought. I feel that either we would tend
towards a lecture course, or we would have to try to get other
participants to present eventually -- which I'm a bit sceptical about!
I could be persuaded, though -- what do other people think?

I think a less rapid pace compared to last year would be good for any format! :)

Joe

[Giles Reger]

Hello all,

I will be near LF15 at 17.00 tomorrow for type-theory related conversation. It is in my calendar!

Joe,

> I'm always thinking of Coq. One advantage of putting IPL first is that
> we couls start coq labs right away on a natural (and well-covered...
> for Coq) topic.

Sounds great!

>> An alternative session style would be to take it in turns to do the reading
>> and then present it back to the group, followed by some discussion. This
>> format would mean we get through more material but would also require more
>> work, but it would be less frequent then last year's format. To encourage
>> newcomers we could draw volunteers to do the reading/presenting from us
>> oldies.
>
> That's an interesting thought. I feel that either we would tend
> towards a lecture course, or we would have to try to get other
> participants to present eventually -- which I'm a bit sceptical about!
> I could be persuaded, though -- what do other people think?

Good point - would be good to hear others opinions on this. If we chose to do the reading "in the session" I think we need at least a couple of people who have read it beforehand to keep conversation going, but without being lecturey.

> I think a less rapid pace compared to last year would be good for any format! :)

I think the problem last year was that our focus was on covering the lecture notes rather than covering a topic. If we switch this around I think our pace will sort itself out.

Giles

[Joseph Razavi]

Hi everyone,

Unfortunately I'm feeling a bit under the weather today, so I won't
make it in -- sorry about the short notice. If there are a few of you
you should still meet, of course,

Joe

P.S.

> I think the problem last year was that our focus was on covering the lecture notes rather than covering a topic. If we switch this around I think our pace will sort itself out.
>

That's a great observation.

[Giles Reger]

Hope you feel better soon Joe - is anybody else planning on turning up?

Giles

[Salman Aljammaz]

I can show up -- if only to say hi.

[Giles Reger]

Salman,

Brilliant - I need to give you money and there was something I wanted to talk to you about anyway!

Giles

On 10 Jul 2012, at 14:42, Salman Aljammaz wrote:

I can show up -- if only to say hi.

[Joseph Razavi]

Hi,

Is anyone around today? Our room is still a bit unfinished-looking, so
just email back and we can meet somewhere. I'll probably go to the
tables nearby at 5 for a few minutes.

I've started editing the wiki page (
http://elearn.cs.man.ac.uk/studact/index.php/Type_Theory_Reading_Group
) -- let me know what you think. You might have a bit of a headache
logging in -- search your CS email for "elearn" to see if you have a
login (I suspect only a crack team of elite superheroes is allowed to
edit it -- in which case I'll change my password and you can all use
my account). It's nowhere near as fancy as the other groups' yet --
but I'm no coder, even in MediaWiki!

Joe

[Francis Southern]

Hello all,

I'm sorry for being so hideously absent in recent weeks, but I am around
today and shall be there if anyone else is!

Francis

[Joseph Razavi]

Hi,

I've just about made it in on time! If anyone's around, I guess the
chairs near our room are the best place...

Joe

On 24 July 2012 13:16, Francis Southern

[Giles Reger]

I'll come down

Giles