Realizability at work: separating two constructive notions of finiteness

DOI10.4230/LIPICS.TYPES.2016.6MaRDI QIDQ6855251zbMATH OpenFDO

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

Publication date 20 February 2026

Copyright license Creative Commons Attribution 3.0 Unported

Full work available at URL https://doi.org/10.4230/LIPICS.TYPES.2016.6

zbMATH Keywords

constructive notions of finitenessrealizabilitytype theory

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites work

• A general formulation of simultaneous inductive-recursive definitions in type theory
• A proof of strong normalisation using domain theory
• Combinatory reduction systems: Introduction and survey
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 5757682 (Why is no real title available?)
• scientific article; zbMATH DE number 3900744 (Why is no real title available?)
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 3231083 (Why is no real title available?)
• scientific article; zbMATH DE number 3077155 (Why is no real title available?)
• Joins in the frame of nuclei
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Recursive models for constructive set theories

This page was built for publication: Realizability at work: separating two constructive notions of finiteness

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6855251)