Type theory (logical and foundational)

Books and Proceedings

1. J. Girard, Y. Lafont, P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1989.

Academic Journals

1. C. Strachey. Fundamental concepts in programming languages. Higher-order and symbolic computation, 13(1):11-49, 2000.
2. Lawrence C. Paulson. Mechanizing Coinduction and Corecursion in Higher-order Logic. J.\ Logic and Computation, 1997.
3. Steffen van Bakel. Complete restrictions of the intersection type discipline. Theoretical Computer Science (TCS), 102:135-163, 1992.
4. Henk Barendregt. Introduction to Generalized Type Systems. J. Funct. Program, 1(2):125-154, 1991.
5. R Backhouse, P. Chisholm, G. Malcolm, E. Saaman. Do-it-Yourself Type Theory. Formal Aspects of Computing, 1(1):19-84, 1989.
6. Michael J. Beeson. Towards a computation system based on set theory. Theoretical Computer Science, 60(3):297-340, 1988.
7. T. Coquand, G. Huet. Calculus of Constructions. Information and Computation, 76:95-120, 1988.
8. R. Statman. Logical Relations and the Typed Lambda Calculus. Information and Control, 65:85-97, 1985.
9. S. Fortune, D. Leivant, M. O'Donnell. The Expressiveness of Simple and Second-Order Type Structures. J. ACM, 30(1):151-185, January 1983.
10. R. Statman. The Typed Lambda Calculus is not Elementary Recursive. Theoretical Computer Science, 9:73-82, 1979.
11. Alonzo Church. A Formulation of the Simple Theory of Types. J. Symb. Log, 5(2):56-68, 1940.

Book Chapters

1. J. Girard. Towards a Geometry of Interaction. In Categories in Computer Science and Logic, Contemporary Mathematics, Volume 92, Scedrov (eds.) Gray (ed.), Contemporary Mathematics, Volume 92, pp. 69-108, American Mathematical Society, 1989.
2. W. Howard. The Formulae-as-Types Notion of Construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. Seldin, J. Hindley (eds.), pp. 479-490, Academic Press, 1980.
3. R. Statman. On the Existence of Closed Terms in the Type Lambda-Calculus I. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. Hindley, J. Seldin (eds.), pp. 511-534, Academic Press, 1980.

International Conferences

1. DeLesley S. Hutchins. Pure subtype systems. In POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Pages 287-298, New York, NY, USA, 2010. download
2. Pawel Urzyczyn. Inhabitation of Low-Rank Intersection Types. In TLCA, Pages 356-370, 2009.
3. J. Polakow, F. Pfenning. Natural deduction for intuitionistic non-commutative linear logic. In Typed Lambda Calculi and Applications, Pages 644-644, 1999.
4. Amy Felty. Encoding the Calculus of Constructions in a Higher-Order Logic. In Proc. Logic in Computer Science (LICS), Montreal, Canada, June 1993.
5. Thierry Coquand. Infinite Objects in Type Theory. In Proc.\ Int'l Workshop on Types for Proofs and Programs (TYPES), Henk Barendregt, Tobias Nipkow (eds.), Lecture Notes in Computer Science (LNCS), Volume 806, Pages 62-78, May 1993.
6. Harry Mairson. A Constructive Logic of Multiple Subtyping. In Proc. 20th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, Pages 313-324, January 1993.
7. Ch. Murthy. A Computational Analysis of Girard's Translation and LC. In Proc. 7th Annual IEEE Symp. on Logic in Computer Science (LICS), Santa Cruz, California, Pages 90-101, June 1992.
8. F. Barbanera, M. Dezani-Ciancaglini. Intersection and Union Types. In Proc. Int'l Conf. on Theoretical Aspects of Computer Software (TACS), Sendai, Japan, T. Ito, A. Meyer (eds.), Lecture Notes in Computer Science, Vol. 526, Pages 651-674, September 1991.
9. R. Constable. Type Theory as a Foundation for Computer Science. In Proc. Int'l Conf. on Theoretical Aspects of Computer Software (TACS), Sendai, Japan, T. Ito, A. Meyer (eds.), Lecture Notes in Computer Science, Vol. 526, Pages 226-243, September 1991.
10. S. Hayashi. Singleton, Union and Intersection Types for Program Extraction. In Proc. Int'l Conf. on Theoretical Aspects of Computer Software (TACS), Sendai, Japan, T. Ito, A. Meyer (eds.), Lecture Notes in Computer Science, Vol. 526, Pages 701-730, September 1991.
11. Z. Luo. ECC, an Extended Calculus of Constructions. In Proc. 1989 IEEE 4th Annual Symp. on Logic in Computer Science (LICS), Pages 385-395, 1989.
12. F. Pfenning. Elf: A Language for Logic Definition and Verified Metaprogramming. In Proc. 1989 IEEE 4th Annual Symp. on Logic in Computer Science (LICS), Pages 313-322, 1989.
13. R. Harper, R. Pollack. Type Checking, Universe Polymorphism, and Typical Ambiguity in the Calculus of Constructions. In Proc. Int'l J't Conf. on Theory and Practice of Software Development (Vol. 2), Lecture Notes in Computer Science, Vo.l. 352, Pages 241-256, Barcelona, Spain, March 1989.
14. C. Paulin-Mohring. Extracting F-omega's Programs from Proofs in the Calculus of Constructions. In Proc. 16th Annual ACM Symp. on Principles of Programming Languages, Pages 89-104, Austin, Texas, January 1989.
15. M. Parigot. Programming with Proofs: A Second-Order Type Theory. In Proc. ESOP '88, Lecture Notes in Computer Science, Vol. 300, Pages 145-159, 1988.
16. D. Howe. Computational Metatheory in Nuprl. In Proc. 9th Int'l Conf. on Automated Deduction, LNCS 310, Pages 238-257, Argonne, Illinois, May 1988.
17. A. Meyer, J. Mitchell, E. Moggi, R. Statman. Empty Types in Polymorphic Lambda Calculus. In Proc. 14th Annual ACM Symp. on Principles of Programming Languages, Pages 253-262, January 1987.
18. T. Coquand. An Analysis of Girard's Paradox. In Proc. IEEE Symp. on Logic in Computer Science (LICS), Pages 227-236, June 1986.
19. A. Meyer, M. Reinhold. `Type' is not a Type. In Proc. 13th ACM Symp. on Principles of Programming Languages, Pages 287-295, St. Petersburg Beach, Florida, January 1986.
20. T. Coquand, G. Huet. Constructions: A Higher Order Proof System for Mechanizing Mathematics. In Proc. European Conf. on Computer Algebra (EUROCAL), Vol. 1 (Invited Lectures), Lecture Notes in Computer Science, Vol. 203, Pages 151-184, April 1985.

Technical Reports

1. Stefano Berardi, Marc Bezem, Thierry Coquand. On the Computational Content of the Axiom of Choice. Research Report Utrecht University, Department of Philosopy, No 116, June 1994.
2. Nick Benton, Gavin Bierman, Valeria de Paiva, Martin Hyland. Term Assignment for Intuitionistic Linear Logic. Research Report Computer Laboratory, University of Cambridge, No 262, August 1992.
3. Ch. Murthy. Classical Proofs as Programs: How, What and Why. Research Report Cornell University, No 91, July 1991.
4. Jean-Yves Girard. A New Constructive Logic: Classical Logic. Programme 2: Calcul Symbolique, Programmation et Génie logiciel INRIA, Rocquencourt, No 1443, June 1991.
5. J. Gallier. Constructive Logics. Part 1: A Tutorial on Proof Systems and Typed Lambda Calculi. Research Report Digital Paris Research Laboratory, No 0, May 1991.
6. J. Gallier. Constructive Logics, Part 2: Linear Logic and Proof Nets. Research Report Digital Paris Research Laboratory, No 0, May 1991.
7. Peter de Bruin. Naturalness of Polymorphism. Research Report U. of Groningen, No 8916, September 1989.
8. T. Coquand. An Analysis of Girard's Paradox. Research Report INRIA, No 0, May 1986.
9. T. Coquand, G. Huet. The Calculus of Constructions. Research Report INRIA, No 0, May 1986.

Miscellaneous

1. R. Backhouse, P. de Bruin, G. Malcolm, J. van der Woude. A Relational Theory of Types. presented at IFIP WG 2.1 meeting at Burton Manor, England, May 1990.
2. J. Girard, A. Scedrov, P. Scott. Bounded Linear Logic - A Modular Approach to Polynomial-Time. Transparencies, 1989.
3. D. Turner. A New Formulation of Constructive Type Theory. Notes from IFIP WG 2.1, 1989.
4. T. Coquand. On the Analogy Between Propositions and Types. Institute on Logical Foundations of Functional Programming (1987 UT Year of Programming), 1987.
5. T. Coquand, G. Huet. A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction. J. Symbolic Computation, Vol. 1, 1985, pp. 323-328, 1985.
6. J. Girard. The System F of Variable Types, Fifteen Years Later. 0.
7. G. Huet. A Uniform Approach to Type Theory. 0.

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.