Reading for Tomorrow

[Joe Razavi]

Hi Everyone,

Reading for tomorrow (not surprisingly) is chapter 6. This chapter
deals with the complexity of some problems related to type checking,
and represents a bit of a detour from the main thrust of the notes.
This should be more familiar ground for computer scientists with a
(slightly) more applied bent, dealing with problems of compiler
implementation rather than foundations and language design; just have
a browse and see what interests you.

See you soon,

Joe

[Giles Reger]

Hi all,

I sadly won't be able to make tomorrow's meeting.

If people are interested in the pragmatic side of type theory then they might want to check out Benjamin C.Pierce's TPAL (Types and Programming Languages) book.

It's quite a slow move through *some* of the stuff we've been looking at - the lambda calculus stuff, not the intuitionistic logic stuff - with a focus on implementation. The implementations he builds up in his book are available online at

http://www.cis.upenn.edu/~bcpierce/tapl/index.html

But it's all in OCaml - which might be an issue for some. If you do want to take a look it's the recon and fullrecon implementations that relate to type reconstruction (sometimes referred to as type inference) - which is the more involved part of Chapter 6.

The fullsimple implementation gives the type checking implementation for the simply typed lambda calculus.

-Giles

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

[Francis Southern]

That's a shame, Giles. I enjoyed your talk about the JVM last week (I
went straight home and disassembled some simple programs) and I was
hoping to ask you some things about it (for example, do you believe that
Java really creates beautiful abstractions? ;-)).

TPAL is definitely a book that's on my radar and OCaml is something I
need to learn more of! Unfortunately I have too much on my plate at the
moment as it is, but I'm currently in the terrifying process of applying
to do PhD at our fine CS department, so maybe that'll give me more time
to devote to such endeavours....

I'd also note that the wonderful Benjamin Pierce has another book, which
is freely (and *ahem* legally) available, called Software Foundations:
http://www.cis.upenn.edu/~bcpierce/sf/
I think it covers some of the same areas as TAPL and is in Coq; I don't
know whether that's better or worse than OCaml...
There is a section on typechecking for the simply-typed lambda calculus
here: http://www.cis.upenn.edu/~bcpierce/sf/Typechecking.html#lab551

Anyway, I'm just procrastinating now...

Francis

[Giles Reger]

Francis,

On 5 Mar 2012, at 12:22, Francis Southern wrote:

That's a shame, Giles.  I enjoyed your talk about the JVM last week (I went straight home and disassembled some simple programs) and I was hoping to ask you some things about it (for example, do you believe that Java really creates beautiful abstractions? ;-)).

We can meet up to talk about it at another time if you want.

On the question you include I might answer

Abstraction is beautiful in the same way that Communism is fair - it looks good until you try and make it work.

TPAL is definitely a book that's on my radar and OCaml is something I need to learn more of!  Unfortunately I have too much on my plate at the moment as it is, but I'm currently in the terrifying process of applying to do PhD at our fine CS department, so maybe that'll give me more time to devote to such endeavours....

Don't worry, you'll definitely have a lot more time on your hands when you start a PhD. 

I'd also note that the wonderful Benjamin Pierce has another book, which is freely (and *ahem* legally) available, called Software Foundations: http://www.cis.upenn.edu/~bcpierce/sf/
I think it covers some of the same areas as TAPL and is in Coq; I don't know whether that's better or worse than OCaml...
There is a section on typechecking for the simply-typed lambda calculus here: http://www.cis.upenn.edu/~bcpierce/sf/Typechecking.html#lab551

Also a very good resource, and seeing as it's freely available probably better. I can't comment on the comparison between OCaml and Coq as I know one but not the other (although hoping to pick up Coq soon). I couldn't see any type reconstruction stuff there - in fact the typing stuff ends with subtyping. However, it does cover exciting things like Hoare Logic, which TAPL doesn't cover, and is a lot more theoretically focussed - so perhaps a more interesting resource for this audience.

Anyway, I'm just procrastinating now...

I prefer to think of it as time-slicing - even low priority processes need a turn to avoid starvation.

Giles

[regerg]

Hello all,

How did discussing the pragmatics of type checking and inference go?

Just to check - are we progressing on to Chapter 7 (The Sequent Calculus)
next week? I want to make sure I make time to read it.

-Giles

On Mon, 5 Mar 2012 12:37:20 +0000, Giles Reger <reg...@cs.man.ac.uk>
wrote:

[Joe Razavi]

Hi,

Yesterday went well thanks :). Indeed, it will be Chapter 7 next week
-- and I probably should send out an official email soon since it
contains cut elimination which people might want to mull over for a
little while.

Joe

> >>> giles.re...@cs.man.ac.uk

> >>> gre...@cantab.net
> >>> 07939 486 756
> >>> *************************
>
> > *************************
> > Giles Reger

> > giles.re...@cs.man.ac.uk