Intuitionistic model constructions and normalization proofs (Q2785696)

This paper aims at giving a semantical treatment to normalization. The idea is to build a nonstandard model, and besides the interpretation function \([\cdot]\) from terms to the model, to define a function quote assigning each element of the model a normal term. Then the normalization process is obtained by the composition of these two functions \(a\to \text{quote} [a]\).NEWLINENEWLINENEWLINEThis is first achieved in the case of Gödel system \({\mathbf T}\). After having defined the semantics and the function quote, the authors prove this indeed gives the normal form, using a glueing technique due to Lafont, related to the glueing construction in cateogry theory. This result is extended to languages having disjoint unions and cartesian products, and to Brouwer ordinals.NEWLINENEWLINENEWLINEThis work is done in an intuitionistic metalanguage: the last section justifies this choice, and relates the formalization to Martin-Löf type theory and to the proof-assistant ALF.