Notes for advanced type systems
Disclaimer: I can't promise that these notes are 100% accurate, or even that I will be able to write them up for every lecture, but I hope they can serve as a useful backup/reference. If you find typos please email adrassi at gmail dot com.
|Notes transcribed from handwritten versions|
|(1/9)|| Proving termination with logical relations|
Correction: closure under beta-expansion can be proved directly by the definition of C[tau]
New material: noted an adjustment to "little gamma in big gamma" judgment when stratifying C over types.
|(...)||Will get TeX'ed ... if someone needs them.|
|(1/23)||Refer to logical relations chapter in ATTAPL|
|Notes after this point are more complete|
|(1/25)||More on equivalence with unit|
|(1/30)|| Even more on equivalence with unit|
I think I've fixed the typos on page 3, but let me know if you spot any.
|(2/1)||Final case for equivalence with unit; Polymorphism|
|(2/6)|| Termination for System F|
Correction: missing little delta in the definition of LR for arrow.
|(2/8)|| Strong normalization for System F|
Correction: fixed mismatches of weak-head and normal reduction towards the end of the notes.
Correction: missing little delta in definition of LR for arrow.
|(2/13)||Finishing proof for SN of System F; Parametricity|
|(2/15)||One more case for SN; One more parametricity example; Girard's J operator|
|(2/22)||More relational parametricity|
|End of notes|
From 2/27 on, we're working out of ATTAPL.
The LaTeX source for these notes is available in a tarball here. Warning: these notes were written during class, so they do not necessarily exhibit beautiful TeX style!
Last updated: Mar 9, 2006