Launching Coq

[Joseph Razavi]

Hi all,

I couldn't straightforwardly book G23, but I don't anticipate any
problems using it. I suggest that we have our first meeting on Monday
5-6 in G23. I'll give a little talk about what we're doing, and then I
think it would be worthwhile just getting people to launch into the
exercises -- and we could wander around giving (something like)
support. I think it's reasonable to aim for the "enumerated types"
section ( http://www.cis.upenn.edu/~bcpierce/sf/Basics.html#lab12 ).
I'll pick out some suggested exercises (and have a serious go at
them!) soon.

We need to do some marketing -- I'll try to do some lecture shout-outs
(also, Giles -- can I shout at people in ManUP this Thursday?) and see
if I can email all the maths undergrads like last year. I also want to
see if I can contact the people doing logic in the philosophy dept. If
anyone wants to do some marketing, just stake out your turf on this
list.

I don't know whether we should tell interested people to use this
address ( manchester-type-th...@googlegroups.com ) as a
point of contact (does it accept emails from outside?) or my address
joseph...@cs.man.ac.uk (the benefit of that is I reply to them all
and we don't get any bystander effect).

I'm up at this time because I really hate writing synopses for emails
-- but it's a necessity of life so here goes:

"

Hi everyone,

Are you interested in logical systems, algorithms, or the foundations
of mathematics?

We're setting up a student type theory group, focussed on working
through selected exercises from the initial chapters of this course:
http://www.cis.upenn.edu/~bcpierce/sf/toc.html . From one point of
view we'll get to grips with Coq, a theorem proving tool which has
seen real mathematical use recently. At the same time, we'll get to
understand some exciting ideas about logic, programming and evidence
in a tangible way.

If you'd like to know more, drop in to our first meeting on Monday 4th
February 5-6pm in room G23 in the Kilburn Building, or contact Joe
(email: joseph...@cs.man.ac.uk mobile: 07583 194 493 ). Please
do get in touch if you're interested (especially if different
arrangements would suit you better.)

See you soon,

Manchester Type Theory Reading Group.

"

Any edits/rewrites welcome!

Joe

P.S. "And everything I forgot!"

[Giles Reger]

Hi Joe,

The timetable says that G23 is free so an email to ro...@cs.man.ac.uk would book it - I'm in the process of booking the ManUP rooms do you want me to contact them about this? Of course you can give a shout out at ManUP on Thursday... we haven't confirmed which room we're in yet.

What are we doing about machines - suggesting people bring laptops or using school machines? If using school machines, did you ask about guest accounts for people not in CS? Is G23 the one with some comfyish chairs on one side of the room and some machines on the other?

I think it's fine giving your details as a point of contact if you're happy to do that - it's useful to have a person who has a vague idea what's going :)

Do we want to include a footnote with rough directions to G23?

Giles

--
You received this message because you are subscribed to the Google Groups "Manchester Type Theory Reading Group" group.
To unsubscribe from this group and stop receiving emails from it, send an email to manchester-type-theory-r...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.

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

Giles,

> The timetable says that G23 is free so an email to ro...@cs.man.ac.uk
> would
> book it - I'm in the process of booking the ManUP rooms do you want me to
> contact them about this? Of course you can give a shout out at ManUP on
> Thursday... we haven't confirmed which room we're in yet.

I went to ACSO and they were a bit cautious about booking out a lab, so
we're emailing a bit as we speak.

> What are we doing about machines - suggesting people bring laptops or
> using
> school machines? If using school machines, did you ask about guest
> accounts
> for people not in CS? Is G23 the one with some comfyish chairs on one side
> of the room and some machines on the other?

This is an important question. I haven't heard anything about my request
to use the guest accounts, so it's best to consider it dead for now. I
think on Monday I'll log in multiple times (or any one of you -- I'm
actually demonstrating right up until 5, so I'll need someone to go in and
set up).

Perhaps for a more sustainable solution we should get people to bring
laptops if they're not from the school -- after all they will probably
want to work on the exercises at home.

It might be worth trying to install Coq on a few OS's so we can hold
people's hands!

> I think it's fine giving your details as a point of contact if you're
> happy
> to do that - it's useful to have a person who has a vague idea what's
> going
> :)

Great, that settles it -- give out my details. (They were on the UMSU
website for 3 years when I was doing the gardening society).

> Do we want to include a footnote with rough directions to G23?

That would probably be a good idea. I've already emailed the poor
philosophers without it (but they can always phone me).

Joe

[Adam Craig Pocock]

Hi everyone,

I've been lurking here since I left Manchester.

It turns out the guy I sit next to at Oracle Labs did his PhD in Coq
related things, and was on the PC in the Coq Workshop last year.
He's Jean-Baptiste Tristan (http://john-tristan.appspot.com/), I think his
group at INRIA wrote the first verified compiler, and his PhD was on
proving different compiler transformations preserve the semantics.

I've asked him if he'd mind corresponding with you guys, I can introduce
you all if you want?

Adam

On Tue, 29 Jan 2013 02:19:03 +0000, Joseph Razavi <jabr...@gmail.com>
wrote:

[Adam Craig Pocock]

First verified C compiler.

Apparently I can't type tonight.

Adam

[Giles Reger]

Hi Adam,

That sounds very useful.

I've read about the verified compiler work before (if it's the work with Xavier Leroy) and found it very interesting - I considered doing a PhD in the area of verifying compiler transformations in the presence of relaxed memory models.

Hope you're enjoying real work.

Giles

[Giles Reger]

Hi,

I'm aware this is starting Monday.

Joe:
- Did we get the room?
- Have we sent the advert to Toby Howard to go in Monday Mail?
- Are we picking out 'suggested' exercises?

Giles

[Joseph Razavi]

Hi,

1) We don't have the room booked; they haven't sent me anything for days.
2) Yep.
3) I'll have a go at that (late) tonight.

We also need someone to go to the room five minutesearly and log in a
few times (and probably start coqide). At the moment I've sort-of
persuaded Francis, but it's not ideal because it'll take up his only
free time!

Any takers?

Joe