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
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