A visiting speaker!

[Francis Southern]

Hello everyone,

I've received an offer from Robin Adams (formerly a student of
Manchester's own Peter Aczel, now a lecturer at Royal Holloway,
University of London) to come and give us a talk about:

“...the crazier parts of the Curry-Howard isomorphism; the parts that
(in my opinion) are not well understood yet:

* control operators correspond to classical logic
* metavariables correspond to modal logic
* and one other that I'll keep a secret until the day of the talk.”

I hope that this sounds exciting to you, so you should tell your friends
and see if we can get a reasonable audience together (more than five
would be nice!). He's said that he's available “pretty much any time
after the 13th of August”, so we can discuss dates, times and locations.

Please let me know what you think,

Francis

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

Sounds very exciting. It would probably be easier to organise a good venue and get a bigger audience if we can arrange it for term time.

Sounds like something we should advertise to staff as well as students, what do people think?

Looking forward to it,
Giles

Sent from my HTC

[Jonas Lorenz]

It sounds very exciting indeed, good work Francis!
If you can schedule the talk after the 23rd of August (and not on the
early afternoon of the 30th) then I will increase the cardinality of
the audience by one.

See you all soon and have a nice summer!
Jonas


On 1 August 2012 17:46, Francis Southern

[Francis Southern]

On 01/08/12 18:20, Jonas Lorenz wrote:
> It sounds very exciting indeed, good work Francis!
> If you can schedule the talk after the 23rd of August (and not on the
> early afternoon of the 30th) then I will increase the cardinality of
> the audience by one.
>
>

I think that should be possible; I look forward to seeing you there
(wherever there is).

On 01/08/12 18:04, reg...@cs.man.ac.uk wrote:
> Sounds very exciting. It would probably be easier to organise a good
> venue and get a bigger audience if we can arrange it for term time.
>

I don't think he's expecting a massive turnout, so I think we should try
for one afternoon between Friday the 24th and Friday the 31st. Any
preferences?

> Sounds like something we should advertise to staff as well as
> students, what do people think?
>

That sounds fine to me. You know the staff (and students, actually)
much better than I do and I think you should bring along anyone you
think might be interested.

I don't really know anything about finding a venue either; does anyone
know whom I'm supposed to talk to about using a room in Kilburn?

Cheers,

Francis

[regerg]

On Fri, 3 Aug 2012 09:38:37 +0100, Francis Southern
<francis....@postgrad.manchester.ac.uk> wrote:
> On 01/08/12 18:20, Jonas Lorenz wrote:
>> It sounds very exciting indeed, good work Francis!
>> If you can schedule the talk after the 23rd of August (and not on the
>> early afternoon of the 30th) then I will increase the cardinality of
>> the audience by one.
>>
>>
> I think that should be possible; I look forward to seeing you there
> (wherever there is).
>
>
> On 01/08/12 18:04, reg...@cs.man.ac.uk wrote:
>> Sounds very exciting. It would probably be easier to organise a good
>> venue and get a bigger audience if we can arrange it for term time.
>>
> I don't think he's expecting a massive turnout, so I think we should try

> for one afternoon between Friday the 24th and Friday the 31st. Any
> preferences?

I'm sadly on a Conference then, followed by 2nd honeymoon until 7th
September. But if you go for then I'll let people know and try and get them
to go along.

>> Sounds like something we should advertise to staff as well as
>> students, what do people think?
>>
> That sounds fine to me. You know the staff (and students, actually)
> much better than I do and I think you should bring along anyone you
> think might be interested.
>
> I don't really know anything about finding a venue either; does anyone
> know whom I'm supposed to talk to about using a room in Kilburn?

I've not done it before, but I think if you just go into ACSO (Academic
Support Office) you can book a room, or perhaps email them. There's
probably an online system too! Are you thinking one of the lecture
theaters? Or just a room? There might even be somebody on this list with
first hand experience of booking rooms!

Giles

[Francis Southern]

I'm sorry I couldn't make it to the meeting yesterday; I had to talk to
my supervisor.

On 03/08/12 10:14, regerg wrote:
> I'm sadly on a Conference then, followed by 2nd honeymoon until 7th
> September. But if you go for then I'll let people know and try and get them
> to go along.
>
>

Hm, that is a shame. Is it impossible for you to make it to any of the
dates Jonas said?
I think Wednesday the 29th is looking most likely otherwise. What do
other people on the list think?

Robin has said that it's fine to invite anyone and everyone; he'll be
giving a brief intro to type theory and Curry-Howard, so no prior
knowledge is required.

If no one on the list has any experience of booking a room to share,
I'll start sending out enquiries soon...


Francis

[Salman Aljammaz]

> If no one on the list has any experience of booking a room to share, I'll
> start sending out enquiries soon...

You can just walk into ACSO and ask one of the staff memebers there. They're
generally very nice. It's in the 2nd floor of Kilburn, first door on
the left, on the corridor right of the stairs from the LF foyer.

[Giles Reger]

Just spoke to future wife and I'm now planning on being in Manchester on Friday 24th so I could do then.

But if that won't work don't worry.

Giles

[Francis Southern]

On 09/08/12 12:14, Giles Reger wrote:

Just spoke to future wife and I'm now planning on being in Manchester on Friday 24th so I could do then.

But if that won't work don't worry.

Giles

Sorry for the long silence, but this has now be confirmed!  It's on Friday the 24th.
I haven't got a time or a room yet; I'll get back with that information as soon as possible (I'm open to suggestions on either).

Also, if anyone wants to go out on the Thursday evening to eat dinner and/or have a few drinks with the speaker that could be fun.

[Salman Aljammaz]

> I haven't got a time or a room yet; I'll get back with that information as
> soon as possible (I'm open to suggestions on either).

It might be useful to let Robert Stevens know, in response to his
email 2 days ago, to help with publicising the event.

[Francis Southern]

I'm afraid I don't think I know who Robert Stevens and I do't think that
I received that email, but any help publicising the event would be
appreciated. Although I haven't got a room or time yet, we know the
date (Friday the 24th) and the speaker (Robin Adams, Royal Holloway,
University of London) and here's the abstract:


The Curry-Howard Isomorphism is the fact that the formal rules for logic
(which deals with propositions and proofs) and type theory (which deals
with programs and types) are identical. There are several opinions on
what this signifies, from the belief that proofs are literally the same
things as programs, to the belief that the isomorphism is just a
coincidence. I shall argue that none of our current explanations for
the Curry-Howard Isomorphism can be entirely correct, by showing three
cases that none of them handles well: the correspondence of control
operators to classical logic, metavariables to modal logic, and the
operation known as the 'zipper' to something completely unexpected
(which I will keep a surprise until the talk!).


Cheers,

Francis

[Giles Reger]

Hi Francis,

Sounds great fun!

Do we have a time for this yet?

Giles

[Francis Southern]

On 21/08/12 12:52, Giles Reger wrote:

Hi Francis,

Sounds great fun!

Do we have a time for this yet?

No, but we really should, shouldn't we?  I sent an email to Robert Stevens yesterday, but haven't heard back.  I'm not sure how long to wait or really what to do next!  I suppose I should go and find ACSO like Salman said.

Francis

[Giles Reger]

Okay,

We can request a booking by emailing  ro...@cs.man.ac.uk but as the person that email goes to is in ACSO this can also be achieved by going directly to their office, which is room 2.127 which you get to by going up the main stairs to the second floor and turning left and then you'll find them in the first room on the left after going through the doors.

If we don't have any other constraints on the time (any constraints people?) we could go for something mid afternoon (the time when most people will be in?) say 14.15 ? - the same time as the school seminars.

In terms of the room we get (which will obviously depend on what's available) I would suggest 2.15 - it's a good size for a small meeting (I don't know if our usual room is back to normal yet).

Just some thoughts,

Giles

[Francis Southern]

On 21/08/12 13:05, Giles Reger wrote:

Okay,

We can request a booking by emailing  ro...@cs.man.ac.uk but as the person that email goes to is in ACSO this can also be achieved by going directly to their office, which is room 2.127 which you get to by going up the main stairs to the second floor and turning left and then you'll find them in the first room on the left after going through the doors.

If we don't have any other constraints on the time (any constraints people?) we could go for something mid afternoon (the time when most people will be in?) say 14.15 ? - the same time as the school seminars.

In terms of the room we get (which will obviously depend on what's available) I would suggest 2.15 - it's a good size for a small meeting (I don't know if our usual room is back to normal yet).

That sounds excellent to me, so if no one objects I'll go into ACSO and ask them about it this afternoon (before the meeting, if there's a meeting?)

[Joseph Razavi]

Is it this Friday? Yegor said so but I thought it was in September. I guess Ian won't be around -- he probably would have gone. Otherwise I bumped into Aczel today -- I said I'd pass on the details as I found them out. He says another type theorist, Gambino, is in town this year.

Joe

[Francis Southern]

Eep, no, it is this Friday, as in he day after tomorrow.  And I'm demonstrating my complete inability to organise my way out of a paper bag!
I didn't make it into uni yesterday, but I emailed rooms@cs this morning and received three automated out-of-office replies, however, I don't know if that means _everyone's_ out of the office or not...

I'm really sorry about all this, but hopefully someone will turn up on Friday.

Francis

[Francis Southern]

Eep, no, it is this Friday, as in he day after tomorrow.  And I'm demonstrating my complete inability to organise my way out of a paper bag!
I didn't make it into uni yesterday, but I emailed rooms@cs this morning and received three automated out-of-office replies, however, I don't know if that means _everyone's_ out of the office or not...

I'm really sorry about all this, but hopefully someone will turn up on Friday.

Francis


On 22/08/12 14:42, Joseph Razavi wrote:

[Joseph Razavi]

I could pop into acso for you? We should really do something to let
people know this is going on. Anyone know which mailing list to spam
to get staff in this department?

I wouldn't worry too much about your organizing skills -- it's not
usually necessary to do everything yourself until you really do know
your way around the system.

Joe

On 22 August 2012 14:56, Francis Southern

[Francis Southern]

I have also sent an email to ac...@cs.etc now, but if you could pop in
that would be appreciated.

Francis

[Joseph Razavi]

Just now? We should give it a few minutes and see if they reply.

On 22 August 2012 15:24, Francis Southern

[Francis Southern]

Yeah, I sent it just after your first email. I'll let you know as soon
as I hear anything from them.

[Francis Southern]

Erm, I didn't hear anything. I don't know whether you went or not, but
if not I'll try my best to go first thing in the morning...

On 22/08/12 15:27, Joseph Razavi wrote:

[Joseph Razavi]

Sorry I didn't reply earlier -- I was afk for an extended period of
time. I didn't go yesterday -- either one of us could go today, but
let me know if it should be me :)

Joe

On 22 August 2012 18:22, Francis Southern

[Francis Southern]

It's completely up to you. If you can (conveniently) make it in the
next hour or so, then it would save me the trip, but if not I'll go then.

Thanks

Francis

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

Right I'll go then -- it will spare me the LaTeX-ing I'm otherwise
embroiled in this morning. Should I go with Giles' suggestion of room 2.15
at 14.15 (if it's available)? (Btw, these numbers are suspiciously
similar...)

Joe

[Joseph Razavi]

Just went to ACSO -- they've got you email. They're having technical
troubles at the moment, so they can't actually book any rooms, but
2.15 is free all day tomorrow. They should send you (Francis) an email
in a little while.

Let me know when plans are as final as they can be, and I'll email a
couple of places where nerds are known to accumulate.

Joe

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

Aww man, I want to come :(

Miss you guys. And your academic ways x

[Francis Southern]

Thanks, Joe! I've received the email and I think it's all as final as
possible. So, let's try and get some people there (Kilburn 2.15)
tomorrow at 14:15!

Thanks again,

[Joseph Razavi]

Francis,

Peter Aczel has asked me whether Robin is staying the night -- how
should I reply? From your previous email is seems like he might be
arriving today -- I'm not sure when he arrives or leaves, and whether
you have any activities planned?

Joe

On 23 August 2012 10:56, Francis Southern

[Francis Southern]

Joe,

He is arriving at around five today and leaving around six tomorrow
evening. I've been too busy panicking about my dissertation to plan
anything, but it could be nice to do something this evening...

Francis

[Salman Aljammaz]

Sorry I've not been very helpful over the past couple of weeks. I've
been experiencing some... downtime.

An email should be sent asap. The usual channel is to ask a member of
staff to send it to one of the mailing lists, but since it's a bit
late to do that we'll have to do it ourselves. People have sent emails
asking for flatshares, help with C++, and advertising seasonal foods.
I don't think this will score very high on the junk spectrum.

These should get to most people:

seminar-di...@cs.man.ac.uk, under...@cs.man.ac.uk,
post...@cs.man.ac.uk

Don't forget to prefix the title with [SEMINAR] or [GUEST TALK]. I've
copied your original email and filled in the gaps in the draft below.
You or Joe or Giles or anyone who's more integral to this group than
me should send it. Modify it as you wish.

--

The Type Theory Reading Group has organised to have a guest talk by
Robin Adams (formerly a student of Manchester's own Peter Aczel, now a
lecturer at Royal Holloway, University of London.)

The talk will be about:

“...the crazier parts of the Curry-Howard isomorphism; the parts that
(in my opinion) are not well understood yet:

* control operators correspond to classical logic
* metavariables correspond to modal logic
* and one other that I'll keep a secret until the day of the talk.”

This will be on Friday 24/8/2012, 2:15pm, room 2.15 in the Kilburn
building. Yes that's tomorrow!

The talk is open for all, regardless of your CS background. I hope
that this sounds exciting to you! See you there & sorry for the late
notice!

--

Regarding dinner tonight, I can suggest Petra on Upper Brook Street.
It's near the university, they serve omnivores, and they don't require
reservations. There's also plenty of other options in the city centre.

Salman

[Joseph Razavi]

Btw, I've sent an email to fm-lunch -- but Salman's suggestions are
all probably better. IPerhaps Francis could email them, so that the
people on fm-lunch don't get two emails from the same guy :P

Joe

[Francis Southern]

I'd just like to thank everyone who came along today and I hope you all
enjoyed it.

I promise to be more together next time!

Francis


P.S. I missed you too, Andy.