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