Semantic analysis of normalisation by evaluation for typed lambda calculus

DOI10.1017/S0960129522000263MaRDI QIDQ5889884

Marcelo P. Fiore

Publication date: 27 April 2023

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

Full work available at URL: https://arxiv.org/abs/2207.08777

zbMATH Keywords

typed lambda calculuslambda definabilityKripke logical relationsnormalisation by evaluationArtin-Wraith glueingalgebraic type theory

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A characterization of lambda definability in categorical models of implicit polymorphism
• Typed lambda calculi and applications. International conference, TLCA '93, March 16--18, 1993, Utrecht, the Netherlands. Proceedings
• Artin glueing
• Strongly typed term representations in Coq
• Intuitionistic model constructions and normalization proofs
• Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums
• Second-Order Equational Logic (Extended Abstract)
• Logical relations and the typed λ-calculus
• Algebraic specification of data types: A synthetic approach
• Normalization and the Yoneda embedding
• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
• Categorical reconstruction of a reduction free normalization proof
• Intensional interpretations of functionals of finite type I
• Types, abstraction, and parametric polymorphism, part 2