Skip to main content
SpringerLink
Log in
Book cover

International Summer School on Applied Semantics

APPSEM 2000: Applied Semantics pp 1–41Cite as

An Introduction to Dependent Type Theory

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2395))

Abstract

Functional programming languages often feature mechanisms that involve complex computations at the level of types. These mechanisms can be analyzed uniformly in the framework of dependent types, in which types may depend on values. The purpose of this chapter is to give some background for such an analysis.

We present here precise theorems, that should hopefully help the reader to understand to which extent statements like “introducing dependent types in a programming language implies that type checking is undecidable”, are justified.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Abel. On relating type theories and set theories. In T. Coquand, P. Dybjer, B. Nordström, and J. Smith, editors, Proceedings of TYPES’99, volume 1956 of Lecture Notes in Computer Science, pages 1–20. Springer-Verlag, 2000.

    Chapter  Google Scholar 

  2. A. Abel. Termination checking with types. Technical Report 0201, Institut fur Informatik, Ludwig-Maximilians-Universität München, 2002.

    Google Scholar 

  3. A. Abel and T. Altenkirch. A predicative analysis of structural recursion. Journal of Functional Programming, 12(1):1–41, January 2002.

    Google Scholar 

  4. P. Aczel. The Type Theoretic Interpretation of Constructive Set Theory. In A. MacIntyre, A. Pacholski, and J. Paris, editors, Proceedings of Logic Colloqium 77, Studies in Logic and the Foundations of Mathematics, pages 55–66. North-Holland, 1978.

    Google Scholar 

  5. P. Aczel. Frege structures and the notions of proposition, truth and set. In J. Barwise, H. J. Keisler, and K. Kunen, editors, Proceedings of the Kleene Symposium, volume 101 of Studies in Logic and the Foundations of Mathematics, pages 31–59. North-Holland, Amsterdam, 1980.

    Google Scholar 

  6. P. Aczel. On Relating Type Theories and Set Theories. In T. Altenkirch, W. Naraschewski, and B. Reus, editors, Proceedings of TYPES’98, volume 1657 of Lecture Notes in Computer Science, pages 1–18. Springer-Verlag, 1999.

    Chapter  Google Scholar 

  7. T. Altenkirch and C. McBride. Generic programming within dependently typed programming. In J. Gibbons and J. Jeuring, editors, Proceedings of WCGP’02. Kluwer Academic Publishers, 2002.

    Google Scholar 

  8. R. Amadio and S. Coupet-Grimal. Analysis of a guard condition in type theory. In M. Nivat, editor, Proceedings of FOSSACS’98, volume 1378 of Lecture Notes in Computer Science, pages 48–62. Springer-Verlag, 1998.

    Google Scholar 

  9. R. M. Amadio and L. Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575–631, September 1993.

    Google Scholar 

  10. D. Aspinall. Subtyping with singleton types. In L. Pacholski and J. Tiuryn, editors, Proceedings of CSL’94, volume 933 of Lecture Notes in Computer Science, pages 1–15. Springer-Verlag, 1994.

    Google Scholar 

  11. P. Audebaud. Partial Objects in the Calculus of Constructions. In Proceedings of LICS’91, pages 86–95. IEEE Computer Society Press, 1991.

    Google Scholar 

  12. L. Augustsson. Cayenne: A language with dependent types. In Proceedings of ICFP’98, pages 239–250. ACM Press, 1998.

    Google Scholar 

  13. L. Augustsson and M. Carlsson. An exercise in dependent types: A well-typed interpreter. In Informal Proceedings of DTP’99, 1999.

    Google Scholar 

  14. R. Backhouse, P. Jansson, J. Jeuring, and L. Meertens. Generic programming— an introduction. In S. D. Swierstra, P. R. Henriques, and J. N. Oliveira, editors, Proceedings of AFP’98, volume 1608 of Lecture Notes in Computer Science, pages 28–115. Springer-Verlag, 1999.

    Google Scholar 

  15. S. van Bakel, L. Liquori, S. Ronchi della Rocca, and P. Urzyczyn. Comparing cubes of typed and type assignment systems. Annals of Pure and Applied Logic, 86(3):267–303, July 1997.

    Google Scholar 

  16. H. Barendregt. Introduction to Generalised Type Systems. Journal of Functional Programming, 1(2):125–154, April 1991.

    Google Scholar 

  17. H. Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, pages 117–309. Oxford Science Publications, 1992. Volume 2.

    Google Scholar 

  18. H. Barendregt and H. Geuvers. Proof assistants using dependent type systems. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume II, chapter 18, pages 1149–1238. Elsevier Publishing, 2001.

    Google Scholar 

  19. G. Barthe. The semi-full closure of Pure Type Systems. In L. Brim, J. Gruska, and J. Zlatuska, editors, Proceedings of MFCS’98, volume 1450 of Lecture Notes in Computer Science, pages 316–325. Springer-Verlag, 1998.

    Google Scholar 

  20. G. Barthe. Type-Checking Injective Pure Type Systems. Journal of Functional Programming, 9(6):675–698, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  21. G. Barthe and T. Coquand. On the equational theory of non-normalizing pure type systems. Journal of Functional Programming, 200x. To appear.

    Google Scholar 

  22. G. Barthe, M. J. Frade, E. Giménez, L. Pinto, and T. Uustalu. Type-based termination of recursive definitions. Mathematical Structures in Computer Science, 2002. To appear.

    Google Scholar 

  23. G. Barthe and M.H. Sørensen. Domain-free pure type systems. Journal of Functional Programming, 10(5):417–452, September 2000.

    Google Scholar 

  24. D. Basin and S. Matthews. Logical Frameworks. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume 9. Kluwer Academic Publishers, 2002.

    Google Scholar 

  25. L.S. van Benthem Jutting. Typing in pure type systems. Information and Computation, 105(1):30–41, July 1993.

    Google Scholar 

  26. L.S. van Benthem Jutting, J. McKinna, and R. Pollack. Checking algorithms for pure type systems. In H. Barendregt and T. Nipkow, editors, Proceedings of TYPES’93, volume 806 of Lecture Notes in Computer Science, pages 19–61. Springer-Verlag, 1994.

    Google Scholar 

  27. G. Betarte. Dependent Record Types and Algebraic Structures in Type Theory. PhD thesis, Department of Computer Science, Chalmers Tekniska Högskola, 1998.

    Google Scholar 

  28. G. Betarte and A. Tasistro. Extension of Martin-Löf’s type theory with record types and subtyping. In G. Sambin and J. Smith, editors, Twenty-five Years of Constructive Type Theory. Oxford University Press, 1998.

    Google Scholar 

  29. R. Bird. Introduction to Functional Programming using Haskell. Prenctice Hall, 2 edition, 1998.

    Google Scholar 

  30. F. Blanqui, J.-P. Jouannaud, and M. Okada. Inductive Data Type Systems. Theoretical Computer Science, 272(1/2):41–68, February 2002.

    Google Scholar 

  31. D. Bolignano. Towards a mechanization of cryptographic protocol verification. In O. Grumberg, editor, Proceedings of CAV’97, volume 1254 of Lecture Notes in Computer Science, pages 131–142. Springer-Verlag, 1997.

    Google Scholar 

  32. M. Brandt and F. Henglein. Coinductive axiomatization of recursive type equality and subtyping. Fundamenta Informaticae, 33(4):309–338, April 1998.

    Google Scholar 

  33. W. Buchholz, S. Feferman, W. Pohlers, and W. Sieg. Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Results, volume 897 of Lectures Notes in Mathematics. Springer-Verlag, 1981.

    Google Scholar 

  34. L. Cardelli. A polymorphic lambda-calculus with Type:Type. Technical Report 10, SRC, May 1986.

    Google Scholar 

  35. L. Cardelli. Phase distinctions in type theory. Unpublished Mansucript, January 1988.

    Google Scholar 

  36. L. Cardelli. Structural subtyping and the notion of power type. In Proceedings of POPL’88, pages 70–79. ACM Press, 1988.

    Google Scholar 

  37. C. Coquand. Agda. See http://www.cs.chalmers.se/~catarina/agda.

  38. C. Coquand. Computation in Type Theory. PhD thesis, Department of Computing Science, Chalmers University of Technology, 1996.

    Google Scholar 

  39. T. Coquand. Metamathematical Investigations of a Calculus of Constructions. In P. Odifreddi, editor, Logic and Computer Science, pages 91–122. Academic Press, 1990.

    Google Scholar 

  40. T. Coquand. An algorithm for testing conversion in type theory. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 255–279. Cambridge University Press, 1991.

    Google Scholar 

  41. T. Coquand. Pattern matching with dependent types. In B. Nordström, editor, Informal proceedings of Logical Frameworks’92, pages 66–79, 1992.

    Google Scholar 

  42. T. Coquand. An algorithm for type-checking dependent types. Science of Computer Programming, 26(1–3):167–177, May 1996.

    Google Scholar 

  43. T. Coquand and P. Dybjer. Inductive definitions and type theory: an introduction (preliminary version). In P.S. Thiagarajan, editor, Proceedings of FSTTCS’94, volume 880 of Lecture Notes in Computer Science, pages 60–76. Springer-Verlag, 1994.

    Google Scholar 

  44. T. Coquand and H. Herbelin. A-translation and looping combinators in pure type systems. Journal of Functional Programming, 4(1):77–88, January 1994.

    Google Scholar 

  45. T. Coquand and G. Huet. The Calculus of Constructions. Information and Computation, 76(2/3):95–120, February/March 1988.

    Google Scholar 

  46. T. Coquand and C. Paulin. Inductively defined types. In P. Martin-Löf and G. Mints, editors, Proceedings of COLOG’88, volume 417 of Lecture Notes in Computer Science, pages 50–66. Springer-Verlag, 1988.

    Google Scholar 

  47. T. Coquand, R. Pollack, and M. Takeyama. Modules as Dependently Typed Records. Manuscript, 2002.

    Google Scholar 

  48. J. Courant. Un calcul de modules pour les systèmes de types purs. PhD thesis, Ecole Normale Supérieure de Lyon, 1998.

    Google Scholar 

  49. G. Cousineau and M. Mauny. The functional approach to programming. Cambridge University Press, 1998.

    Google Scholar 

  50. K. Crary. Sound and complete elimination of singleton kinds. In R. Harper, editor, Proceedings of TIC’00, volume 2071 of Lecture Notes in Computer Science, pages 1–26. Springer-Verlag, 2001.

    Google Scholar 

  51. K. Crary and S. Weirich. Resource bound certification. In Proceedings of POPL’00, pages 184–198. ACM Press, 2000.

    Google Scholar 

  52. P. Dybjer. Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 280–306. Cambridge University Press, 1991.

    Google Scholar 

  53. P. Dybjer. Inductive families. Formal Aspects of Computing, 6:440–465, 1994.

    Article  MATH  Google Scholar 

  54. P. Dybjer. Representing inductively defined sets by well-orderings in Martin-Löf’s type theory. Theoretical Computer Science, 176(1–2):329–335, April 1997.

    Google Scholar 

  55. P. Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65(2):525–549, June 2000.

    Google Scholar 

  56. H. Geuvers. Logics and type systems. PhD thesis, University of Nijmegen, 1993.

    Google Scholar 

  57. H. Geuvers. Induction is not derivable in second order dependent type theory. In S. Abramsky, editor, Proceedings of TLCA’01, Lecture Notes in Computer Science, pages 166–181. Springer-Verlag, 2001.

    Google Scholar 

  58. H. Geuvers and M.J. Nederhof. A modular proof of strong normalisation for the Calculus of Constructions. Journal of Functional Programming, 1(2):155–189, April 1991.

    Google Scholar 

  59. H. Geuvers, E. Poll, and J. Zwanenburg. Safe proof checking in type theory with Y. In J. Flum and M. Rodríguez-Artalejo, editors, Proceedings of CSL’99, volume 1683 of Lecture Notes in Computer Science, pages 439–452. Springer-Verlag, 1999.

    Google Scholar 

  60. H. Geuvers and B. Werner. On the Church-Rosser property for expressive type systems and its consequence for their metatheoretic study. In Proceedings of LICS’94, pages 320–329. IEEE Computer Society Press, 1994.

    Google Scholar 

  61. J. Giesl, C. Walther, and J. Brauburger. Termination analysis for functional programs. In W. Bibel and P. Schmitt, editors, Automated Deduction-A Basis for Applications, volume 3 of Applied Logic Series, pages 135–164. Kluwer Academic Publishers, 1998.

    Google Scholar 

  62. E. Giménez. Un calcul de constructions infinies et son application à la vérification de systèmes communicants. PhD thesis, Ecole Normale Superieure de Lyon, 1996.

    Google Scholar 

  63. E. Giménez. Structural recursive definitions in Type Theory. In K.G. Larsen, S. Skyum, and G. Winskel, editors, Proceedings of ICALP’98, volume 1443 of Lecture Notes in Computer Science, pages 397–408. Springer-Verlag, 1998.

    Google Scholar 

  64. J-Y. Girard. Interprétation fonctionnelle et élimination des coupures dans l’arithmétique d’ordre supérieur. Thèse d’Etat, Université Paris 7, 1972.

    Google Scholar 

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

    Google Scholar 

  66. B. Grégoire and X. Leroy. A compiled implementation of strong reduction. In Proceedings of ICFP’02. ACM Press, 2002.

    Google Scholar 

  67. B. Grobauer. Cost recurrences for DML programs. In Proceedings of ICFP’01, pages 253–264. ACM Press, September 2001.

    Google Scholar 

  68. P. Hancock and A. Setzer. Interactive programs in dependent type theory. In P. Clote and H. Schwichtenberg, editors, Proceedings of CSL’00, volume 1862 of Lecture Notes in Computer Science, pages 317–331. Springer-Verlag, 2000.

    Google Scholar 

  69. R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143–184, January 1993.

    Google Scholar 

  70. R. Harper, J. C. Mitchell, and E. Moggi. Higher-order modules and the phase distinction. In Proceedings of POPL’90, pages 341–354. ACM Press, 1990.

    Google Scholar 

  71. R. Harper and J.C. Mitchell. On the type structure of Standard ML. ACM Transactions on Programming Languages and Systems, 15(2):211–252, April 1993.

    Google Scholar 

  72. R. Hinze. A new approach to generic functional programming. In Proceedings of POPL’00, pages 119–132. ACM Press, 2000.

    Google Scholar 

  73. J. G. Hook and D. J. Howe. Impredicative strong existential equivalent to type:type. Technical Report TR86-760, Cornell University, Computer Science Department, June 1986.

    Google Scholar 

  74. J. Hughes, L. Pareto, and A. Sabry. Proving the correctness of reactive systems using sized types. In Proceedings of POPL’96, pages 410–423. ACM Press, 1996.

    Google Scholar 

  75. A. Hurkens. A Simplification of Girard’s Paradox. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of TLCA’ 95, volume 902 of Lecture Notes in Computer Science, pages 266–278. Springer-Verlag, 1995.

    Google Scholar 

  76. P. Jansson and J. Jeuring. PolyP—a polytypic programming language extension. In Proceedings of POPL’97, pages 470–482. ACM Press, 1997.

    Google Scholar 

  77. S. Jha, J. Palsberg, and T. Zhao. Efficient type matching. In M. Nielsen and U. Engberg, editors, Proceedings of FOSSACS 2002, volume 2303 of Lecture Notes in Computer Science, pages 187–204. Springer-Verlag, 2002.

    Google Scholar 

  78. M. P. Jones. Type classes with functional dependencies. In G. Smolka, editor, Proceedings of ESOP’00, volume 1782 of Lecture Notes in Computer Science, pages 230–244, 2000.

    Google Scholar 

  79. J.-P. Jouannaud and M. Okada. Abstract data type systems. Theoretical Computer Science, 173(2):349–391, February 1997.

    Google Scholar 

  80. D. Kozen, J. Palsberg, and M. Schwartzback. Efficient recursive subtyping. Mathematical Structures in Computer Science, 5(1):113–125, March 1995.

    Google Scholar 

  81. B. Lampson and R. Burstall. Pebble, a kernel language for modules and abstract data types. Information and Computation, 76(2/3):278–346, February/March 1988.

    Google Scholar 

  82. C.-S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change principle for program termination. In Proceedings of POPL’01, pages 81–92. ACM Press, 2001.

    Google Scholar 

  83. X. Leroy. A modular module system. Journal of Functional Programming, 10(3):269–303, May 2000.

    Google Scholar 

  84. G. Longo and E. Moggi. Constructive natural deduction and its ‘w-set’ interpretation. Mathematical Structures in Computer Science, 1(2):215–254, July 1991.

    Google Scholar 

  85. Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. Number 11 in International Series of Monographs on Computer Science. Oxford University Press, 1994.

    Google Scholar 

  86. Z. Luo. Coercive subtyping. Journal of Logic and Computation, 9(1):105–130, February 1999.

    Google Scholar 

  87. D. MacQueen. Using dependent types to express modular structure. In Proceedings of POPL’86, pages 277–286. ACM Press, 1986.

    Google Scholar 

  88. L. Magnusson. The implementation of ALF: a proof editor based on Martin-Löf’s monomorphic type theory with explicit substitution. PhD thesis, Department of Computer Science, Chalmers University, 1994.

    Google Scholar 

  89. P. Martin-Löf. Hauptsatz for the intuitionistic theory of iterated inductive definitions. In J. E. Fenstad, editor, Proceedings 2nd Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics, pages 179–216. North-Holland, Amsterdam, 1971.

    Google Scholar 

  90. P. Martin-Löf. A theory of types. Technical Report, Stockholm University, February 1971.

    Google Scholar 

  91. P. Martin-Löf. An intuitionistic theory of types. Unpublished Manuscript, 1972.

    Google Scholar 

  92. P. Martin-Löf. Intuitionistic Type Theory, volume 1 of Studies in Proof Theory. Bibliopolis, Naples, 1984.

    Google Scholar 

  93. P. Martin-Löf. Constructive mathematics and computer programming. In C. A. R. Hoare and J. C. Shepherdson, editors, Mathematical Logic and Programming Languages, pages 167–184. Prentice-Hall, 1985.

    Google Scholar 

  94. C. McBride. Dependently typed functional programs and their proofs. PhD thesis, University of Edinburgh, 2000.

    Google Scholar 

  95. C. McBride. Faking It (Simulating Dependent Types in Haskell). Journal of Functional Programming, 2002. To appear.

    Google Scholar 

  96. N. P. Mendler. Inductive types and type constraints in second-order lambda calculus. In Proceedings of LICS’87, pages 30–36. IEEE Computer Society Press, 1987.

    Google Scholar 

  97. N. P. Mendler. Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic, 51(1–2):159–172, March 1991.

    Google Scholar 

  98. R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, 1978.

    Article  MATH  MathSciNet  Google Scholar 

  99. R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. The MIT Press, 1991.

    Google Scholar 

  100. R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). The MIT Press, 1997.

    Google Scholar 

  101. A. Miquel. The implicit calculus of constructions. In S. Abramsky, editor, Proceedings of TLCA’01, volume 2044 of Lecture Notes in Computer Science, pages 344–359. Springer-Verlag, 2001.

    Google Scholar 

  102. A. Miquel. Le Calcul des Constructions implicite: syntaxe et sémantique. PhD thesis, Université Paris 11, 2001.

    Google Scholar 

  103. J. C. Mitchell and G. D. Plotkin. Abstract types have existential type. ACM Transactions on Programming Languages and Systems, 10(3):470–502, July 1988.

    Google Scholar 

  104. G. C. Necula. Proof-carrying code. In Proceedings of POPL’97, pages 106–119. ACM Press, 1997.

    Google Scholar 

  105. G. C. Necula and P. Lee. Efficient representation and validation of logical proofs. In Proceedings of LICS’98, pages 93–104, 1998.

    Google Scholar 

  106. R. Nederpelt, H. Geuvers, and R. de Vrijer, editors. Selected Papers on Automath, volume 133 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1994.

    Google Scholar 

  107. M. Neubauer, P. Thiemann, M. Gasbichler, and M. Sperber. Functional logic overloading. In Proceedings of POPL’02, pages 233–244. ACM Press, 2002.

    Google Scholar 

  108. B. Nordström. Terminating general recursion. BIT, 28(3):605–619, 1988.

    Article  MATH  MathSciNet  Google Scholar 

  109. B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf’s Type Theory. An Introduction. Number 7 in International Series of Monographs on Computer Science. Oxford University Press, 1990.

    Google Scholar 

  110. J. Palsberg and T. Zhao. Efficient and flexible matching of recursive types. Information and Computation, 171:364–387, November 2001.

    Google Scholar 

  111. L. Pareto. Types for crash prevention. PhD thesis, Department of Computing, Chalmers Tekniska Högskola, 2000.

    Google Scholar 

  112. C. Paulin-Mohring. Inductive definitions in the system Coq. Rules and properties. In M. Bezem and J.F. Groote, editors, Proceedings of TLCA’ 93, volume 664 of Lecture Notes in Computer Science, pages 328–345. Springer-Verlag, 1993.

    Google Scholar 

  113. C. Paulin-Mohring. Définitions Inductives en Theorie des Types d’Ordre Superieur. Habilitation à diriger les recherches, Université Claude Bernard Lyon I, 1996.

    Google Scholar 

  114. L. C. Paulson. ML for the Working Programmer. Cambridge University Press, 1996.

    Google Scholar 

  115. L.C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6(1/2):85–128, 1998.

    Google Scholar 

  116. S. Peyton Jones and E. Meijer. Henk: a typed intermediate language. Appeared as Technical Report BCCS-97-03, Computer Science Department, Boston College, 1997.

    Google Scholar 

  117. H. Pfeifer and H. Rueß. Polytypic abstraction in type theory. In R. Backhouse and T. Sheard, editors, Informal Proceedings of WGP’98. Department of Computing Science, Chalmers University, June 1998.

    Google Scholar 

  118. H. Pfeifer and H. Rueß. Polytypic proof construction. In Y. Bertot, G. Dowek, H. Hirshowitz, C. Paulin, and L. Théry, editors, Proceedings of TPHOLs’99, volume 1690 of Lecture Notes in Computer Science, pages 55–72. Springer-Verlag, 1999.

    Google Scholar 

  119. F. Pfenning. Elf: a meta-language for deductive systems. In A. Bundy, editor, Proceedings of CADE-12, volume 814 of Lecture Notes in Artificial Intelligence, pages 811–815. Springer-Verlag, 1994.

    Google Scholar 

  120. F. Pfenning. Logical Frameworks. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume II, chapter 17, pages 1063–1147. Elsevier Publishing, 2001.

    Google Scholar 

  121. F. Pfenning and C. Paulin. Inductively Defined Types in the Calculus of Constructions. In M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Proceedings of MFPS’89, volume 442 of Lecture Notes in Computer Science, pages 209–228. Springer-Verlag, 1989.

    Google Scholar 

  122. R. Pollack. Typechecking in pure type systems. In B. Nordström, editor, Informal proceedings of Logical Frameworks’92, pages 271–288, 1992.

    Google Scholar 

  123. R. Pollack. The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1994.

    Google Scholar 

  124. R. Pollack. Dependently typed records for representing mathematical structures. In M. Aagard and J. Harrison, editors, Proceedings of TPHOLs’00, volume 1869 of Lecture Notes in Computer Science, pages 462–479. Springer-Verlag, 2000.

    Google Scholar 

  125. M. B. Reinhold. Typechecking is undecidable’ TYPE’ is a type. Technical Report MIT/LCS/TR-458, Massachusetts Institute of Technology, December 1989.

    Google Scholar 

  126. D. Rémy. Using, Understanding, and Unraveling the OCaml Language—From Practice to Theory and vice versa. This volume.

    Google Scholar 

  127. J. W. Roorda. Pure Type Systems for Functional Programming. Master’s thesis, Department of Computer Science, University of Utrecht, 2000.

    Google Scholar 

  128. C. Russo. Types For Modules. PhD thesis, University of Edinburgh, 1998.

    Google Scholar 

  129. A. Salvesen and J. Smith. The Strength of the Subset Type in Martin-Löf’s Type Theory. In Proceedings of LICS’88, pages 384–391. IEEE Computer Society Press, 1988.

    Google Scholar 

  130. D. Scott. Constructive validity. In M. Laudet, D. Lacombe, L. Nolin, and M. Schützenberger, editors, Proceedings of Symposium on Automatic Demonstration, volume 125 of Lecture Notes in Mathematics, pages 237–275. Springer-Verlag, 1970.

    Google Scholar 

  131. P. Severi. Type Inference for Pure Type Systems. Information and Computation, 143(1):1–23, May 1998.

    Google Scholar 

  132. Z. Shao, B. Saha, V. Trifonov, and N. Papaspyrou. A type system for certified binaries. In Proceedings of POPL’02, pages 217–232. ACM Press, 2002.

    Google Scholar 

  133. M. H. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Available as DIKU Rapport 98/14, 1998.

    Google Scholar 

  134. M. Stefanova and H. Geuvers. A simple set-theoretic semantics for the Calculus of Constructions. In S. Berardi and M. Coppo, editors, Proceedings of TYPES’95, volume 1158 of Lecture Notes in Computer Science, pages 249–264. Springer-Verlag, 1996.

    Google Scholar 

  135. C. A. Stone and R. Harper. Deciding Type Equivalence with Singleton Kinds. In Proceedings of POPL’00, pages 214–227. ACM Press, 2000.

    Google Scholar 

  136. M. D. G. Swaen. Weak and strong sum elimination in intuitionistic type theory. PhD thesis, Faculty of Mathematics and Computer Science, University of Amsterdam, 1989.

    Google Scholar 

  137. W. W. Tait. Constructive reasoning. In Proceedings of the Third International Congress in Logic, Methodology and Philosophy of Science, pages 185–199. North-Holland Publishing, 1968.

    Google Scholar 

  138. S. Thompson. Haskell. The Craft of Functional Programming. Addison-Wesley, 1996.

    Google Scholar 

  139. D. Walker. A Type System for Expressive Security Policies. In Proceedings of POPL’00, pages 254–267. ACM Press, 2000.

    Google Scholar 

  140. B. Werner. Sets in Types, Types in Sets. In M. Abadi and T. Ito, editors, Proceedings of TACS’97, volume 1281 of Lecture Notes in Computer Science, pages 530–546. Springer-Verlag, 1997.

    Google Scholar 

  141. H. Xi. Dependent types in practical programming. PhD thesis, Department of Computer Science, Carnegie-Mellon University, 1998.

    Google Scholar 

  142. H. Xi. Dead Code Elimination through Dependent Types. In G. Gupta, editor, Proceedings of PADL’99, volume 1551, pages 228–242. Springer-Verlag, 1999.

    Google Scholar 

  143. H. Xi and R. Harper. A Dependently Typed Assembly Language. In Proceedings of ICFP’01, pages 169–180. ACM Press, 2001.

    Google Scholar 

  144. H. Xi and F. Pfenning. Eliminating array bound checking through dependent types. In Proceedings of PLDI’98, pages 249–257. ACM Press, 1998.

    Google Scholar 

  145. H. Xi and F. Pfenning. Dependent types in practical programming. In Proceedings of POPL’99, pages 214–227. ACM Press, 1999.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Sophia-Antipolis, France

    Gilles Barthe

  2. Institutionen för Datavetenskap, Chalmers Tekniska Högskola, Göteborg, Sweden

    Thierry Coquand

Authors
  1. Gilles Barthe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thierry Coquand
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Projet Lemme, INRIA Sophia-Antipolis, 2004 Route des Lucioles, BP 93, 06902, Sophia Antipolis Cedex, France

    Gilles Barthe

  2. Department of Computing Science, Chalmers University of Technology, 412 96, Göteborg, Sweden

    Peter Dybjer

  3. Departamento de Matemática, Universidade do Minho, Campus de Gualtar, 4710-057, Braga, Portugal

    Luís Pinto

  4. Departamento de Informática, Universidade do Minho, Campus de Gualtar, 4710-057, Braga, Portugal

    João Saraiva

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Barthe, G., Coquand, T. (2002). An Introduction to Dependent Type Theory. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds) Applied Semantics. APPSEM 2000. Lecture Notes in Computer Science, vol 2395. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45699-6_1

Download citation

  • DOI: https://doi.org/10.1007/3-540-45699-6_1

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44044-4

  • Online ISBN: 978-3-540-45699-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation