References

[1] Henk Barendregt. Lambda calculi with types. In Samson Abramsky, D. M. Gabbai, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2. Oxford University Press, 1991.

[2] Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Cambridge University Press, 1989.

[3] Healfdene Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, August 1994.

[4] Zhaohui Luo. Computation and Reasoning. Oxford University Press, 1994.

[5] Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.

[6] John Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science. North Holland, 1990.

[7] Bengt Nordström, Kent Petersson, and Jan Smith. Programming in Martin-Löf’s Type Theory: An Introduction. Oxford University Press, 1990.

[8] L. van Benthem Jutting, James McKinna, and Robert Pollack. Typechecking in pure type systems. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programming. Springer–Verlag, 1993.