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.
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
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
On 5 Mar 2012, at 11:19, Joe Razavi wrote:
> 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.
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
> 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
> 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
> On 5 Mar 2012, at 11:19, Joe Razavi wrote:
>> 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.
> 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.
> On 05/03/12 11:51, Giles Reger wrote: >> 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
>> 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
>> On 5 Mar 2012, at 11:19, Joe Razavi wrote:
>>> 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.
> 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
>> Francis
>> On 05/03/12 11:51, Giles Reger wrote: >>> 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
>>> 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
>>> On 5 Mar 2012, at 11:19, Joe Razavi wrote:
>>>> 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.
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
On Mar 7, 11:48 am, regerg <reg...@cs.man.ac.uk> wrote:
> 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:
> > 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
> >> Francis
> >> On 05/03/12 11:51, Giles Reger wrote:
> >>> 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
> >>> 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
> >>> On 5 Mar 2012, at 11:19, Joe Razavi wrote:
> >>>> 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.
