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/4) Strengthening induction
(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/20) Relational parametricity
(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!

Back home

Last updated: Mar 9, 2006