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