Intuitionistic model constructions and normalization proofs

DOI10.1017/S0960129596002150MaRDI QIDQ2785696zbMATH OpenWikidataFDO

Authors Thierry Coquand, Peter Dybjer

Publication date 23 March 1998

Published in MSCS. Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/S0960129596002150

zbMATH Keywords

Brouwer ordinalsglueingintuitionistic metalanguageMartin-Löf type theorynormalizationproof-assistant ALFsemantics

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Second- and higher-order arithmetic and fragments (03F35) Semantics in the theory of computing (68Q55)

Review text

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.

Recommendations

• Strong normalization in type systems: A model theoretical approach
• Denotational aspects of untyped normalization by evaluation
• scientific article; zbMATH DE number 512774
• Program extraction from normalization proofs
• Foundations of Software Science and Computation Structures

Cited in

(23)

• Term rewriting for normalization by evaluation.
• A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\)
• A context-based approach to proving termination of evaluation
• The simple type theory of normalisation by evaluation
• On Normalization by Evaluation for Object Calculi
• Big-step normalisation
• Typed Applicative Structures and Normalization by Evaluation for System F ω
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids
• Internal type theory
• Models of intuitionistic TT and NF
• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
• Categorical reconstruction of a reduction free normalization proof
• Normalization by Evaluation for Typed Weak lambda-Reduction
• Denotational aspects of untyped normalization by evaluation
• A logical framework combining model and proof theory
• Semantic analysis of normalisation by evaluation for typed lambda calculus
• Normalization by evaluation for modal dependent type theory
• Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation
• Representing model theory in a type-theoretical logical framework
• Categorical structure in coherent theory of arithmetic
• Intuitionistic validity in \(T\)-normal Kripke structures
• Program extraction from normalization proofs

This page was built for publication: Intuitionistic model constructions and normalization proofs

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