A Compiled Implementation of Normalization by Evaluation

DOI10.1007/978-3-540-71067-7_8MaRDI QIDQ3543648zbMATH OpenOpenAlexFDO

Authors Klaus Aehlig, Florian Haftmann, Tobias Nipkow

Publication date 4 December 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71067-7_8

Mathematics Subject Classification ID

Recommendations

• A compiled implementation of normalisation by evaluation
• The simple type theory of normalisation by evaluation
• Typeful normalization by evaluation
• Operational aspects of untyped Normalisation by Evaluation
• Normalisation by evaluation for type theory, in type theory

Cites work

• scientific article; zbMATH DE number 1670733 (Why is no real title available?)
• scientific article; zbMATH DE number 2018582 (Why is no real title available?)
• scientific article; zbMATH DE number 1552508 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• A compiled implementation of strong reduction
• Automated Deduction – CADE-20
• Flyspeck I: Tame Graphs
• Nominal logic, a first order theory of names and binding
• Normalization by evaluation with typed abstract syntax
• Operational aspects of untyped Normalisation by Evaluation
• Partial Recursive Functions in Higher-Order Logic
• Term rewriting for normalization by evaluation.
• The Four Colour Theorem: Engineering of a Formal Proof

Cited in

(14)

• Flyspeck II: The basic linear programs
• Normalization by evaluation and algebraic effects
• scientific article; zbMATH DE number 1757129 (Why is no real title available?)
• Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
• Operational aspects of untyped Normalisation by Evaluation
• The Isabelle Framework
• Normalisation by evaluation for type theory, in type theory
• Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq
• On theorem prover-based testing
• A compiled implementation of normalisation by evaluation
• Typeful normalization by evaluation
• Normalisation by evaluation for dependent types
• scientific article; zbMATH DE number 5353378 (Why is no real title available?)
• Typed Applicative Structures and Normalization by Evaluation for System F ω

Describes a project that uses

Uses Software

• Tame Graphs
• Nominal Isabelle
• Flyspeck
• KIV
• HOL
• ML

This page was built for publication: A Compiled Implementation of Normalization by Evaluation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3543648)