Big-step normalisation
From MaRDI portal
Publication:3638919
DOI10.1017/S0956796809007278zbMath1191.68153WikidataQ61583831 ScholiaQ61583831MaRDI QIDQ3638919
James T. E. Chapman, Thorsten Altenkirch
Publication date: 28 October 2009
Published in: Journal of Functional Programming (Search for Journal in Brave)
Related Items (7)
Indexed containers ⋮ Pure type systems with explicit substitutions ⋮ Unnamed Item ⋮ Structural recursion with locally scoped names ⋮ Type Theory Should Eat Itself ⋮ Normalization by Evaluation for Typed Weak lambda-Reduction ⋮ Towards a Cubical Type Theory without an Interval
Cites Work
- Unnamed Item
- Normalization without reducibility
- A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
- Intuitionistic model constructions and normalization proofs
- Extensional Rewriting with Sums
- The view from the left
- The virtues of eta-expansion
- Intensional interpretations of functionals of finite type I
This page was built for publication: Big-step normalisation
