Realizability at Work: Separating Two Constructive Notions of Finiteness

Authors Marc Bezem, Thierry Coquand, Keiko Nakata, Erik Parmann

Thumbnail PDF


  • Filesize: 0.5 MB
  • 23 pages

Document Identifiers

Author Details

Marc Bezem
Thierry Coquand
Keiko Nakata
Erik Parmann

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)


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.
  • Type theory
  • realizability
  • constructive notions of finiteness


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


  1. M. Beeson. Recursive models for constructive set theories. Annals of Mathematical Logic, 23:127-178, 1982. Google Scholar
  2. M. J. Beeson. Foundations of Constructive Mathematics, volume 6 of Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer, 1985. Google Scholar
  3. T. Coquand and A. Spiwack. A proof of strong normalisation using domain theory. Logical Methods in Computer Science, 3(4), 2007. Google Scholar
  4. 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. Google Scholar
  5. P. Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65(2):525-549, 2000. Google Scholar
  6. M. Escardó. Joins in the frame of nuclei. Applied Categorical Structures, 11:117-124, 2003. Google Scholar
  7. 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. Google Scholar
  8. 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. Google Scholar
  9. 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. Google Scholar
  10. E. Parmann. URL:
  11. E. Parmann. Case Studies in Constructive Mathematics. PhD thesis, University of Bergen, 2016. Google Scholar
  12. 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. Google Scholar
  13. 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. Google Scholar
  14. A. S. Troelstra, editor. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics. Springer, 1973. Google Scholar
  15. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. The Univalent Foundations Program, Institute for Advanced Study, 2013. URL:
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