![]() |
![]() |
We define a logical framework with singleton types and one universe of small types. We give the semantics using a PER model; it is used for constructing a normalisation-by-evaluation algorithm. We prove completeness and soundness of the algorithm; and get as a corollary the injectivity of type constructors. Then we give the definition of a correct and complete type-checking algorithm for terms in normal form. We extend the results to proof-irrelevant propositions.
Source : ScholeXplorer
IsCitedBy ARXIV 2110.13704 Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.types.2020.6
Hondet, Gabriel ; Blanqui, Frédéric ; |