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!
Last updated: Mar 9, 2006