Extensionality of lambda-*

Author Andrew Polonsky

Thumbnail PDF


  • Filesize: 0.6 MB
  • 30 pages

Document Identifiers

Author Details

Andrew Polonsky

Cite AsGet BibTex

Andrew Polonsky. Extensionality of lambda-*. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 221-250, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


We prove an extensionality theorem for the "type-in-type" dependent type theory with Sigma-types. We suggest that in type theory the notion of extensional equality be identified with the logical equivalence relation defined by induction on type structure.
  • Extensionality
  • logical relations
  • type theory
  • lambda calculus
  • reflection


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Thorsten Altenkirch. Extensional equality in intensional type theory. In LICS, pages 412-420. IEEE Computer Society, 1999. Google Scholar
  2. Robert Atkey, Neil Ghani, and Patricia Johann. A relationally parametric model of dependent type theory. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'14, pages 503-515, New York, NY, USA, 2014. ACM. Google Scholar
  3. H. P. Barendregt. Lambda calculi with types. In S. Abramsky, Dov M. Gabbay, and S. E. Maibaum, editors, Handbook of Logic in Computer Science (Vol. 2), pages 117-309. Oxford University Press, Inc., New York, NY, USA, 1992. Google Scholar
  4. Jean-Philippe Bernardy and Marc Lasson. Realizability and parametricity in pure type systems. In Martin Hofmann, editor, Foundations of Software Science and Computational Structures, volume 6604 of Lecture Notes in Computer Science, pages 108-122. Springer Berlin Heidelberg, 2011. Google Scholar
  5. Thierry Coquand. Equality and dependent type theory, 2011. URL: http://www.cse.chalmers.se/~coquand/equality.pdf.
  6. Peter Dybjer and Anton Setzer. Indexed induction-recursion. In Reinhard Kahle, Peter Schroeder-Heister, and Robert Stärk, editors, Proof Theory in Computer Science, volume 2183 of Lecture Notes in Computer Science, pages 93-113. Springer Berlin Heidelberg, 2001. Google Scholar
  7. Neil Ghani, Lorenzo Malatesta, Fredrik Nordvall Forsberg, and Anton Setzer. Fibred data types. In LICS, pages 243-252. IEEE Computer Society, 2013. Google Scholar
  8. F. Rabe and K. Sojakova. Logical Relations for a Logical Framework. ACM Transactions on Computational Logic, 2013. to appear. Google Scholar
  9. William W. Tait. Extensional equality in the classical theory of types. In Werner Depauli-Schimanovich, Eckehart Köhler, and Friedrich Stadler, editors, The Foundational Debate, volume 3 of Vienna Circle Institute Yearbook [1995], pages 219-234. Springer Netherlands, 1995. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail