eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-11-05
6:1
6:23
10.4230/LIPIcs.TYPES.2016.6
article
Realizability at Work: Separating Two Constructive Notions of Finiteness
Bezem, Marc
Coquand, Thierry
Nakata, Keiko
Parmann, Erik
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol097-types2016/LIPIcs.TYPES.2016.6/LIPIcs.TYPES.2016.6.pdf
Type theory
realizability
constructive notions of finiteness