Next Semester...
6 views
Skip to first unread message
Giles Reger
Dec 29, 2012, 6:46:12 AM12/29/12
to manchester-type-th...@googlegroups.com
... I think we should start meeting again.
A question is when? As I haven't received my teaching timetable yet,
and we may well move ManUP again, I'm not sure when I'm free yet.
The next question is what?
I wanted to explore Coq - not having done anything with it before. I
found these notes
http://www.seas.upenn.edu/~cis500/current/sf/index.html
can anybody with some familiarity with Coq (Joe?) look and see if
they're appropriate?
Alternatively, whilst looking I found these lists of papers that
formed the reading for an advanced course in programming languages -
we could work through some of these:
http://www.seas.upenn.edu/~cis670/Spring2003/
http://www.seas.upenn.edu/~sweirich/cis670/10/
Hope you are all well,
Giles
A question is when? As I haven't received my teaching timetable yet,
and we may well move ManUP again, I'm not sure when I'm free yet.
The next question is what?
I wanted to explore Coq - not having done anything with it before. I
found these notes
http://www.seas.upenn.edu/~cis500/current/sf/index.html
can anybody with some familiarity with Coq (Joe?) look and see if
they're appropriate?
Alternatively, whilst looking I found these lists of papers that
formed the reading for an advanced course in programming languages -
we could work through some of these:
http://www.seas.upenn.edu/~cis670/Spring2003/
http://www.seas.upenn.edu/~sweirich/cis670/10/
Hope you are all well,
Giles
raza...@cs.man.ac.uk
Jan 4, 2013, 6:55:50 PM1/4/13
to manchester-type-th...@googlegroups.com
Giles!
> ... I think we should start meeting again.
>
> A question is when?
Those of us with no exams (you and I?) should meet soon I think -- if only
to share enthusiasm. (There might also be some plumbing we could take care
of before the semester strikes...)
> As I haven't received my teaching timetable yet,
> and we may well move ManUP again, I'm not sure when I'm free yet.
>
> The next question is what?
>
> I wanted to explore Coq - not having done anything with it before. I
> found these notes
>
> http://www.seas.upenn.edu/~cis500/current/sf/index.html
>
> can anybody with some familiarity with Coq (Joe?) look and see if
> they're appropriate?
These pages have restored my belief that we can do something useful. I
think if we can get people through much of that, we'll have given them
something highly worthwhile.
In particular, we would ideally do the sections Basic to Logic (Can this
be done in one semester?). I think that would be a good jumping off point
to talk about Curry-Howard, predicativity etc. I think it would be a nice
experiment to see if we can do Basic -- Logic (or a cut down version) in a
semester, then next year we could do it in the first semester (and perhaps
with some other experienced people around who we trained this year!) and
use it as a springboard into all sorts of weird stuff in the second
(perhaps I'm getting ahead of myself...)
> Alternatively, whilst looking I found these lists of papers that
> formed the reading for an advanced course in programming languages -
> we could work through some of these:
> http://www.seas.upenn.edu/~cis670/Spring2003/
> http://www.seas.upenn.edu/~sweirich/cis670/10/
These look great too! (Though I haven't had time to look in detail) It
would be nice to have some reading alongside the Coq. I wonder whether a
nice general model (at least for now) would be to use Coq as a unifying
activity, and launch reading groups off it in an ad-hoc fashion. More
experienced members could list and remark on interesting-looking papers
(on the wiki perhaps, if I can fix the permissions), and we could go
through any which people find particularly interesting in detail (and peer
at syntax together). Thoughts?
Thank you thank you thank you thank you!
Joe
> ... I think we should start meeting again.
>
> A question is when?
to share enthusiasm. (There might also be some plumbing we could take care
of before the semester strikes...)
> As I haven't received my teaching timetable yet,
> and we may well move ManUP again, I'm not sure when I'm free yet.
>
> The next question is what?
>
> I wanted to explore Coq - not having done anything with it before. I
> found these notes
>
> http://www.seas.upenn.edu/~cis500/current/sf/index.html
>
> can anybody with some familiarity with Coq (Joe?) look and see if
> they're appropriate?
think if we can get people through much of that, we'll have given them
something highly worthwhile.
In particular, we would ideally do the sections Basic to Logic (Can this
be done in one semester?). I think that would be a good jumping off point
to talk about Curry-Howard, predicativity etc. I think it would be a nice
experiment to see if we can do Basic -- Logic (or a cut down version) in a
semester, then next year we could do it in the first semester (and perhaps
with some other experienced people around who we trained this year!) and
use it as a springboard into all sorts of weird stuff in the second
(perhaps I'm getting ahead of myself...)
> Alternatively, whilst looking I found these lists of papers that
> formed the reading for an advanced course in programming languages -
> we could work through some of these:
> http://www.seas.upenn.edu/~cis670/Spring2003/
> http://www.seas.upenn.edu/~sweirich/cis670/10/
would be nice to have some reading alongside the Coq. I wonder whether a
nice general model (at least for now) would be to use Coq as a unifying
activity, and launch reading groups off it in an ad-hoc fashion. More
experienced members could list and remark on interesting-looking papers
(on the wiki perhaps, if I can fix the permissions), and we could go
through any which people find particularly interesting in detail (and peer
at syntax together). Thoughts?
Thank you thank you thank you thank you!
Joe
Francis Southern
Jan 5, 2013, 4:23:50 AM1/5/13
to manchester-type-th...@googlegroups.com
I've been meaning to reply as well, sorry. I'm not sure I can add much
to the discussion at the moment, except to say that I am alive and
interested in meeting in the coming semester, I have got exams so I'm a
little preoccupied for the next fortnight, and I pretty much agree with
everything Joe said!
Francis
regerg
Jan 7, 2013, 1:03:59 PM1/7/13
to manchester-type-th...@googlegroups.com
X! for some X in {Joe, Francis}
Good Stuff.
>> Giles!
>>
>>> ... I think we should start meeting again.
>>>
>>> A question is when?
>> Those of us with no exams (you and I?) should meet soon I think -- if
>> only
>> to share enthusiasm. (There might also be some plumbing we could take
>> care of before the semester strikes...)
How about an enthusiasm sharing session tomorrow (Tuesday)?
That sounds great. I think we could manage Basic to Logic - a lot of it
looks like relating concepts a lot of us will be familiar with to Coq
concepts. Maybe we should meet in a room with machines if we're going to be
a .... 'practical' theory group. Although we could take the approach of
coding together on the screen (very hip and happening I hear).
>>> Alternatively, whilst looking I found these lists of papers that
>>> formed the reading for an advanced course in programming languages -
>>> we could work through some of these:
>>> http://www.seas.upenn.edu/~cis670/Spring2003/
>>> http://www.seas.upenn.edu/~sweirich/cis670/10/
>> These look great too! (Though I haven't had time to look in detail) It
>> would be nice to have some reading alongside the Coq. I wonder whether
a
>> nice general model (at least for now) would be to use Coq as a unifying
>> activity, and launch reading groups off it in an ad-hoc fashion. More
>> experienced members could list and remark on interesting-looking papers
>> (on the wiki perhaps, if I can fix the permissions), and we could go
>> through any which people find particularly interesting in detail (and
>> peer
>> at syntax together). Thoughts?
We could have an after-school club for the Coq stuff and a lunch-time club
for the reading stuff?
>> Thank you thank you thank you thank you!
>>
>> Joe
>>
>>
>
> Hi,
>
> I've been meaning to reply as well, sorry. I'm not sure I can add much
> to the discussion at the moment, except to say that I am alive
Yay :)
> and interested in meeting in the coming semester, I have got exams so
I'm a
> little preoccupied for the next fortnight, and I pretty much agree with
> everything Joe said!
>
> Francis
Giles
Good Stuff.
>> Giles!
>>
>>> ... I think we should start meeting again.
>>>
>>> A question is when?
>> Those of us with no exams (you and I?) should meet soon I think -- if
>> only
>> to share enthusiasm. (There might also be some plumbing we could take
>> care of before the semester strikes...)
looks like relating concepts a lot of us will be familiar with to Coq
concepts. Maybe we should meet in a room with machines if we're going to be
a .... 'practical' theory group. Although we could take the approach of
coding together on the screen (very hip and happening I hear).
>>> Alternatively, whilst looking I found these lists of papers that
>>> formed the reading for an advanced course in programming languages -
>>> we could work through some of these:
>>> http://www.seas.upenn.edu/~cis670/Spring2003/
>>> http://www.seas.upenn.edu/~sweirich/cis670/10/
>> These look great too! (Though I haven't had time to look in detail) It
>> would be nice to have some reading alongside the Coq. I wonder whether
a
>> nice general model (at least for now) would be to use Coq as a unifying
>> activity, and launch reading groups off it in an ad-hoc fashion. More
>> experienced members could list and remark on interesting-looking papers
>> (on the wiki perhaps, if I can fix the permissions), and we could go
>> through any which people find particularly interesting in detail (and
>> peer
>> at syntax together). Thoughts?
for the reading stuff?
>> Thank you thank you thank you thank you!
>>
>> Joe
>>
>>
>
> Hi,
>
> I've been meaning to reply as well, sorry. I'm not sure I can add much
> to the discussion at the moment, except to say that I am alive
> and interested in meeting in the coming semester, I have got exams so
I'm a
> little preoccupied for the next fortnight, and I pretty much agree with
> everything Joe said!
>
> Francis
Joseph Razavi
Jan 7, 2013, 1:16:59 PM1/7/13
to manchester-type-th...@googlegroups.com
Giles,
> That sounds great. I think we could manage Basic to Logic - a lot of it
> looks like relating concepts a lot of us will be familiar with to Coq
> concepts.
I was thinking with some newbies -- how possible do you think that is?
> Maybe we should meet in a room with machines if we're going to be
> a .... 'practical' theory group. Although we could take the approach of
> coding together on the screen (very hip and happening I hear).
I think we should get a room with machines (especially if we want
newbies). this is the kind of "plumbing" we could deal with while the
others worry about their exams.
> We could have an after-school club for the Coq stuff and a lunch-time club
> for the reading stuff?
The difficulty here with undergrads is that they don't have a fixed
lunchtime. But if we launch with Coq only, and then chat about a
reading group, then we might be able to find a free lunchtime.
You and I should definitely meet on Tuesday (tomorrow).
> X! for some X in {Joe, Francis}
exists Joe. Qed.
> That sounds great. I think we could manage Basic to Logic - a lot of it
> looks like relating concepts a lot of us will be familiar with to Coq
> concepts.
> Maybe we should meet in a room with machines if we're going to be
> a .... 'practical' theory group. Although we could take the approach of
> coding together on the screen (very hip and happening I hear).
newbies). this is the kind of "plumbing" we could deal with while the
others worry about their exams.
> We could have an after-school club for the Coq stuff and a lunch-time club
> for the reading stuff?
lunchtime. But if we launch with Coq only, and then chat about a
reading group, then we might be able to find a free lunchtime.
You and I should definitely meet on Tuesday (tomorrow).
> X! for some X in {Joe, Francis}
regerg
Jan 7, 2013, 1:23:57 PM1/7/13
to manchester-type-th...@googlegroups.com
On Mon, 7 Jan 2013 18:16:59 +0000, Joseph Razavi <jabr...@gmail.com>
wrote:
polymorphism, but higher-order functions might slow us down... but will be
very useful for them. Of course if they come to all the Scala-related stuff
happening in ManUP this term they'll find it easy ;)
We should just go for it, aim high and then slow down if necessary.
>> Maybe we should meet in a room with machines if we're going to be
>> a .... 'practical' theory group. Although we could take the approach of
>> coding together on the screen (very hip and happening I hear).
>
> I think we should get a room with machines (especially if we want
> newbies). this is the kind of "plumbing" we could deal with while the
> others worry about their exams.
Good idea.
>> We could have an after-school club for the Coq stuff and a lunch-time
>> club
>> for the reading stuff?
>
> The difficulty here with undergrads is that they don't have a fixed
> lunchtime. But if we launch with Coq only, and then chat about a
> reading group, then we might be able to find a free lunchtime.
>
> You and I should definitely meet on Tuesday (tomorrow).
What time is good for you?
>> X! for some X in {Joe, Francis}
>
> exists Joe. Qed.
=> Joe!
wrote:
> Giles,
>
>> That sounds great. I think we could manage Basic to Logic - a lot of it
>> looks like relating concepts a lot of us will be familiar with to Coq
>> concepts.
>
> I was thinking with some newbies -- how possible do you think that is?
I suppose it depends how new - Lists should be fine and hopefully
>
>> That sounds great. I think we could manage Basic to Logic - a lot of it
>> looks like relating concepts a lot of us will be familiar with to Coq
>> concepts.
>
> I was thinking with some newbies -- how possible do you think that is?
polymorphism, but higher-order functions might slow us down... but will be
very useful for them. Of course if they come to all the Scala-related stuff
happening in ManUP this term they'll find it easy ;)
We should just go for it, aim high and then slow down if necessary.
>> Maybe we should meet in a room with machines if we're going to be
>> a .... 'practical' theory group. Although we could take the approach of
>> coding together on the screen (very hip and happening I hear).
>
> I think we should get a room with machines (especially if we want
> newbies). this is the kind of "plumbing" we could deal with while the
> others worry about their exams.
>> We could have an after-school club for the Coq stuff and a lunch-time
>> club
>> for the reading stuff?
>
> The difficulty here with undergrads is that they don't have a fixed
> lunchtime. But if we launch with Coq only, and then chat about a
> reading group, then we might be able to find a free lunchtime.
>
> You and I should definitely meet on Tuesday (tomorrow).
>> X! for some X in {Joe, Francis}
>
> exists Joe. Qed.
Joseph Razavi
Jan 7, 2013, 4:45:54 PM1/7/13
to manchester-type-th...@googlegroups.com
I'm free all day -- though I might be a bit hard to find in the
morning! If you want to fix a time, shall we say 2pm in the postgrad
common room (I'll probably be working in the CDT lab all day). You can
change this arbitrarily, or just drop in.
Joe
morning! If you want to fix a time, shall we say 2pm in the postgrad
common room (I'll probably be working in the CDT lab all day). You can
change this arbitrarily, or just drop in.
Joe
Joseph Razavi
Jan 8, 2013, 8:38:38 AM1/8/13
to manchester-type-th...@googlegroups.com
Hi -- I'm going to be a bit late!
Giles Reger
Jan 8, 2013, 8:39:21 AM1/8/13
to manchester-type-th...@googlegroups.com
Okay - I will be there from 2 but will have to leave by 3
Giles
On 8 Jan 2013, at 13:38, Joseph Razavi wrote:
Hi -- I'm going to be a bit late!
*************************
Giles Reger
07939 486 756
*************************
Reply all
Reply to author
Forward
0 new messages