Semantic analysis of normalisation by evaluation for typed lambda calculus
From MaRDI portal
Publication:5889884
DOI10.1017/S0960129522000263MaRDI QIDQ5889884
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
typed lambda calculuslambda definabilityKripke logical relationsnormalisation by evaluationArtin-Wraith glueingalgebraic type theory
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