A Compiled Implementation of Normalization by Evaluation
From MaRDI portal
Publication:3543648
DOI10.1007/978-3-540-71067-7_8zbMath1165.68442OpenAlexW1538801588MaRDI QIDQ3543648
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (5)
Flyspeck II: The basic linear programs ⋮ A compiled implementation of normalisation by evaluation ⋮ On theorem prover-based testing ⋮ The Isabelle Framework ⋮ Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
Uses Software
Cites Work
- Term rewriting for normalization by evaluation.
- Nominal logic, a first order theory of names and binding
- A compiled implementation of strong reduction
- Normalization by evaluation with typed abstract syntax
- The Four Colour Theorem: Engineering of a Formal Proof
- Flyspeck I: Tame Graphs
- Partial Recursive Functions in Higher-Order Logic
- Operational aspects of untyped Normalisation by Evaluation
- Automated Deduction – CADE-20
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: A Compiled Implementation of Normalization by Evaluation
