LIPIcs.TYPES.2014.221.pdf
- Filesize: 0.6 MB
- 30 pages
Document
Extensionality of lambda-*
Author
-
Part of:
Volume:
20th International Conference on Types for Proofs and Programs (TYPES 2014)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Types for Proofs and Programs (TYPES) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2015-10-12
Cite As Get 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)
https://doi.org/10.4230/LIPIcs.TYPES.2014.221
Abstract
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.
Subject Classification
Keywords
- Extensionality
- logical relations
- type theory
- lambda calculus
- reflection
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Thorsten Altenkirch. Extensional equality in intensional type theory. In LICS, pages 412-420. IEEE Computer Society, 1999.
-
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.
-
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.
-
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.
- Thierry Coquand. Equality and dependent type theory, 2011. URL: http://www.cse.chalmers.se/~coquand/equality.pdf.
-
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.
-
Neil Ghani, Lorenzo Malatesta, Fredrik Nordvall Forsberg, and Anton Setzer. Fibred data types. In LICS, pages 243-252. IEEE Computer Society, 2013.
-
F. Rabe and K. Sojakova. Logical Relations for a Logical Framework. ACM Transactions on Computational Logic, 2013. to appear.
-
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.