The Simple Type Theory of Normalisation by Evaluation

DOI10.1016/S1571-0661(04)00272-5zbMath1268.68056MaRDI QIDQ2841227

René Vestergaard

Publication date: 24 July 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Combining algebraic rewriting, extensional lambda calculi, and fixpoints
• Intuitionistic model constructions and normalization proofs
• Normalization and the Yoneda embedding
• Thunks and the λ-calculus
• The virtues of eta-expansion
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The Simple Type Theory of Normalisation by Evaluation