Thesis
Note: the thesis is easier to read when printed in color.
Change History
Nov 30: initial draft
Dec 5 : new section on local definitions (Chapter 5)
Dec 19: revised Chapters 1 & 2
Dec 20: revised Chapter 3
Dec 24: added a section on Russell- and Tarski-style universes (Section 5.2.5)
Dec 24: revised Chapter 4
Dec 26: revised Section 5.1
Jan 5 : revised Sections 5.2 - 5.5
Jan 7 : revised Chapter 6
Jan 12 : revised Chapters 7 - 8; switched to a CBV target language (Chapter 4); added Appendix
Jan 17 : GADT & refinement types (Section 1.1.4); classical laws and control operators (Section 7.3)
Jan 23 : type-returning CPS (Section 5.2.4)
Feb 18: minor revisions
Mar 12: finalish version
Mar 23: submitted version
Mar 31: final version