| Autor: |
Bezem, Marc, Coquand, Thierry, Nakata, Keiko, Parmann, Erik |
| Jazyk: |
angličtina |
| Rok vydání: |
2018 |
| Předmět: |
|
| DOI: |
10.4230/lipics.types.2016.6 |
| Popis: |
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. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
