Bibliography: Topics in Type Theory

Primary 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] Robert Pollack. The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh, April 1995.

[9] 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.

   Also, see the pages http://www.dcs.ed.ac.uk/lfcsinfo/research/types bra/index.html
and file:/usr/local/share/www/packages/lego/index.html.

Secondary References

[1] Thorsten Altenkirch. Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh, November 1993.

[2] C. Böhm and A. Berarducci. Automatic synthesis of typed λ-programs on term algebras. Theoretical Computer Science, 39, 1985.

[3] Adriana Compagnoni. Higher-Order Subtyping with Intersection Types. PhD thesis, University of Nijmegen, 1995.

[4] Robert L. Constable, et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice–Hall, Englewood Cliffs, NJ, 1986.

[5] Thierry Coquand. An analysis of Girard’s paradox. In Proc. of the Symposium on Logic in Computer Science, pages 227–236, Boston, June 1986.

[6] Thierry Coquand and Jean Gallier. A proof of strong normalization for the theory of constructions using a Kripke-like interpretation. In Workshop on Logical Frameworks– Preliminary Proceedings, 1990.

[7] Peter Dybjer. Inductively defined sets in Martin-Löf’s set theory. In Arnon Avron et al., editors, Workshop on General Logic. Dept. of Computer Science, University of Edinburgh, 1988.

[8] Peter Dybjer. Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks. Cambridge University Press, 1991.

[9] Philippa A. Gardner. Representing Logics in Type Theory. PhD thesis, University of Edinburgh, 1992.

[10] Herman Geuvers. Logics and Type Systems. PhD thesis, Katholieke Universiteit Nijmegen, September 1993.

[11] Herman Geuvers and Benjamin Werner. On the Church–Rosser property for expressive type systems and its consequences for their metatheoretic study. In Symposium on Logic in Computer Science, pages 320–329, Paris, France, July 1994. IEEE Computer Society Press.

[12] Robert Harper, Furio Honsell, and Gordon D. Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143–184, 1992.

[13] Robert Harper and Robert Pollack. Type checking with universes. Theoretical Computer Science, 89, 1991.

[14] J. Hook and D. Howe. Impredicative strong existential equivalent to Type:Type. Technical Report TR86-760, Cornell University, 1986.

[15] Per Martin-Löf. A theory of types. Unpublished manuscript, 1971.

[16] Per Martin-Löf. An intuitionistic theory of types: Predicative part. In H. Rose and J. C. Shepherdson, editors, Logic Colloqium 1973, pages 73–118, 1975.

[17] Per Martin-Löf. Constructive mathematics and computer programming. In L. J. Cohen et al., editors, Logic, Methodology and Philosophy of Science VI, Amsterdam, 1982. North-Holland.

[18] Per Martin-Löf. Substitution calculus. Handwritten notes, 1992.

[19] R.P. Nederpelt, J.H. Geuvers, and editors R.C. de Vrijer. Selected Papers on AUTOMATH, volume 133 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1994.

[20] Anne Salvesen. On Information Discharging and Retrieval in Martin-Löf’s Type Theory. PhD thesis, University of Oslo, March 1989.

[21] Anne Salvesen. The Church-Rosser property for pure type systems with βη-reduction, November 1991. Unpublished manuscript.

[22] Jan Smith. The independence of Peano’s fourth axiom from Martin-Löf’s type theory without universes. Journal of Symbolic Logic, 53(3), 1988.

[23] Jan Smith. An interpretation of kleene’s slash in type theory. In Gérard Huet and Gordon Plotkin, editors, Logical Environments, pages 189–197. Cambridge University Press, 1993.

[24] Søren Stenlund. Combinators, λ-calculus and Proof Theory. D. Reidel, Dordrecht, 1972.

[25] Masako Takahashi. Parallel reductions in λ-calculus. Information and Computation, 118:120–127, 1995.

[26] L.S. van Benthem Jutting. Typing in Pure Type Systems. Information and Computation, 105(1):30–41, July 1993.