LIPIcs.TYPES.2016.6.pdf
- Filesize: 0.5 MB
- 23 pages
Document
Realizability at Work: Separating Two Constructive Notions of Finiteness
Authors
-
Part of:
Volume:
22nd International Conference on Types for Proofs and Programs (TYPES 2016)
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: 2018-11-05
Cite AsGet BibTex
Marc Bezem, Thierry Coquand, Keiko Nakata, and Erik Parmann. Realizability at Work: Separating Two Constructive Notions of Finiteness. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.TYPES.2016.6
https://doi.org/10.4230/LIPIcs.TYPES.2016.6
Abstract
We elaborate in detail a realizability model for Martin-Löf dependent type theory with the purpose to analyze a subtle distinction between two constructive notions of finiteness of a set A. The two notions are: (1) A is Noetherian: the empty list can be constructed from lists over A containing duplicates by a certain inductive shortening process; (2) A is streamless: every enumeration of A contains a duplicate.
Keywords
- Type theory
- realizability
- constructive notions of finiteness
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
M. Beeson. Recursive models for constructive set theories. Annals of Mathematical Logic, 23:127-178, 1982.
-
M. J. Beeson. Foundations of Constructive Mathematics, volume 6 of Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer, 1985.
-
T. Coquand and A. Spiwack. A proof of strong normalisation using domain theory. Logical Methods in Computer Science, 3(4), 2007.
-
T. Coquand and A. Spiwack. Constructively finite? In L. Lambán, A. Romero, and J. Rubio, editors, Contribuciones científicas en honor de Mirian Andrés Gómez, pages 217-230. Publicaciones de la Universidad de La Rioja, 2010. ISBN 978-84-96487-50-5.
-
P. Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65(2):525-549, 2000.
-
M. Escardó. Joins in the frame of nuclei. Applied Categorical Structures, 11:117-124, 2003.
-
S.C. Kleene. Recursive functions and intuitionistic mathematics. In L.M. Graves, E. Hille, P.A. Smith, and O. Zariski, editors, Proceedings of the International Congress of Mathematicians, pages 679-685. AMS, 1952.
-
J. W. Klop, V. van Oostrom, and F. van Raamsdonk. Combinatory reduction systems: Introduction and survey. Theoretical Computer Science, 121(1&2):279-308, 1993.
-
P. Martin-Löf. An intuitionistic theory of types: predicative part. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium '73, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73-118, Amsterdam, 1975. North-Holland.
- E. Parmann. URL: https://github.com/epa095/noetherian-implies-streamless.
-
E. Parmann. Case Studies in Constructive Mathematics. PhD thesis, University of Bergen, 2016.
-
D. Pataraia. A constructive proof of Tarski’s fixed-point theorem for DCPOs. Presented at the 65th Peripatetic Seminar on Sheaves and Logic, November 1997.
-
C. Spector. Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics. In J.C.E. Dekker, editor, Recursive function theory, Proc. Symp. in pure mathematics V, pages 1-27. AMS, 1962.
-
A. S. Troelstra, editor. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics. Springer, 1973.
- The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. The Univalent Foundations Program, Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book.