A compiled implementation of normalisation by evaluation

DOI10.1017/S0956796812000019zbMath1248.68130MaRDI QIDQ2913943

Klaus Aehlig, Florian Haftmann, Tobias Nipkow

Publication date: 21 September 2012

Published in: Journal of Functional Programming (Search for Journal in Brave)

zbMATH Keywords

ML-like languages

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Functional programming and lambda calculus (68N18)

Related Items (1)

A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem

Uses Software

• Isabelle
• Isabelle/HOL

Cites Work

• Unnamed Item
• Term rewriting for normalization by evaluation.
• Isabelle/HOL. A proof assistant for higher-order logic
• A Compiled Implementation of Normalization by Evaluation
• Flyspeck I: Tame Graphs
• Partial Recursive Functions in Higher-Order Logic
• Operational aspects of untyped Normalisation by Evaluation

This page was built for publication: A compiled implementation of normalisation by evaluation