Intuitionistic model constructions and normalization proofs

DOI10.1017/S0960129596002150zbMath0883.03009WikidataQ129355992 ScholiaQ129355992MaRDI QIDQ2785696

Thierry Coquand, Peter Dybjer

Publication date: 23 March 1998

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

zbMATH Keywords

normalizationsemanticsMartin-Löf type theoryglueingBrouwer ordinalsintuitionistic metalanguageproof-assistant ALF

Mathematics Subject Classification ID

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

Related Items (19)

Semantic analysis of normalisation by evaluation for typed lambda calculus ⋮ Categorical reconstruction of a reduction free normalization proof ⋮ Denotational aspects of untyped normalization by evaluation ⋮ On Normalization by Evaluation for Object Calculi ⋮ Normalization by evaluation for modal dependent type theory ⋮ Term rewriting for normalization by evaluation. ⋮ Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation ⋮ Representing model theory in a type-theoretical logical framework ⋮ A logical framework combining model and proof theory ⋮ Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids ⋮ Internal type theory ⋮ A Context-based Approach to Proving Termination of Evaluation ⋮ Big-step normalisation ⋮ Normalization by Evaluation for Typed Weak lambda-Reduction ⋮ Typed Applicative Structures and Normalization by Evaluation for System F ω ⋮ The Simple Type Theory of Normalisation by Evaluation ⋮ A type- and scope-safe universe of syntaxes with binding: their semantics and proofs ⋮ A general formulation of simultaneous inductive-recursive definitions in type theory ⋮ Program extraction from normalization proofs

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