---
title: "The Isabelle Framework — paper by Wenzel et al. (2008)"
description: "The authors propose a compiled variant of Normalization by Evaluation (NBE). 18 references, cited by 21 papers here."
authors: ["Makarius Wenzel", "Lawrence C. Paulson", "Tobias Nipkow"]
year: 2008
venue: "TPHOLs 2008, LNCS 5170, 33–38"
source: "https://www21.in.tum.de/~nipkow/pubs/"
doi: "10.1007/978-3-540-71067-7_7"
licence: "author's copy — read only"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/wenzel-2008-isabelle-framework/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/wenzel-2008-isabelle-framework/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2008](https://md.research.elamur.ai/free/en/papers/2008/) / The Isabelle Framework

# The Isabelle Framework

**Authors:** Makarius Wenzel, [Lawrence C. Paulson](https://md.research.elamur.ai/free/en/authors/lawrence-c-paulson/) and [Tobias Nipkow](https://md.research.elamur.ai/free/en/authors/tobias-nipkow/) · **Year:** 2008 · **Venue:** [TPHOLs 2008, LNCS 5170, 33–38](https://md.research.elamur.ai/free/en/venues/lecture-notes-in-computer-science/) ([Lecture notes in computer science 2008](https://md.research.elamur.ai/free/en/venues/lecture-notes-in-computer-science/2008/)) · **Publisher:** [Springer Science+Business Media](https://md.research.elamur.ai/free/en/publishers/springer-science-business-media/) · **Licence:** author's copy — read only

**Links:** [Publisher's page](https://doi.org/10.1007/978-3-540-71067-7_7) · [PDF](https://www21.in.tum.de/~nipkow/pubs/tphols08.pdf) · [DOI 10.1007/978-3-540-71067-7\_7](https://doi.org/10.1007/978-3-540-71067-7_7) · [OpenAlex](https://openalex.org/W1571434026)

**Citations:** 162 citations (OpenAlex, 2026-10-14) · [21](https://md.research.elamur.ai/free/en/papers/wenzel-2008-isabelle-framework/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
**Note:** the supplied text is not "The Isabelle Framework" (Wenzel, Paulson, Nipkow). It is "A Compiled Implementation of Normalization by Evaluation" by Klaus Aehlig, Florian Haftmann and Tobias Nipkow, and this summary covers that text.

Theorem provers need fast symbolic normalization of terms under user-supplied rewrite rules, including open terms with free variables. The authors propose a compiled variant of Normalization by Evaluation (NBE). Isabelle terms are translated into ML code over an untyped universal datatype `Univ`, so ML itself handles substitution and pattern matching. Results are then read back into terms through eta expansion, and types are reconstructed afterwards. Functions that cannot reduce further are treated as additional constructors, which allows open terms and higher-order rules such as associativity. The approach is formally modelled and verified in Isabelle/HOL, and the correctness argument does not depend on any type system. It ships with Isabelle 2007 both as a normalizer and as a proof rule. Benchmarks show NBE runs one to two orders of magnitude faster than the simplifier and only moderately slower than closed-term evaluation, a good balance of speed and expressiveness.

## Key points
- **Universal datatype:** `Univ` has three constructors, `Const`, `Var` and `Clo`. Application is a separate `apply` function rather than a constructor, because values stand for normal terms only.
- **Benchmarks (ms; simp / nbe_s / nbe / eval):**
  - eras: 4304 / 339 / 311 / 48
  - graph: 222,717 / 3312 / 1953 / 292
  - sort: 1,451,169 / 11,174 / 6453 / 393
  - Setup: Isabelle 2007, PolyML 5.1, Linux 2.6, AMD 1 GHz.
- **Constant identification:** using integers rather than strings for constant names in patterns noticeably speeds up NBE (nbe vs. nbe_s).
- **Comparison with eval:** eval is limited to closed terms and constructor-only results, and it cannot use extra rules like associativity. NBE removes all three restrictions.
- **Availability and future work:** the formalization is in the Archive of Formal Proofs (afp.sf.net). Planned extensions include non-left-linear, ordered and conditional rewriting, plus a possible nominal re-verification in place of de Bruijn indices.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [University of Cambridge](https://md.research.elamur.ai/free/en/universities/university-of-cambridge/) — University, Cambridge, United Kingdom · 287 works · 125,174 citations
- [Technical University of Munich](https://md.research.elamur.ai/free/en/universities/technical-university-of-munich/) — University, Munich, Germany · 66 works · 49,493 citations

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: Makarius Wenzel, Lawrence C. Paulson and Tobias Nipkow. 2008. The Isabelle Framework. TPHOLs 2008, LNCS 5170, 33–38.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@inproceedings{wenzel2008isabelle,
  title = {{The Isabelle Framework}},
  author = {Makarius Wenzel, Lawrence C. Paulson and Tobias Nipkow},
  booktitle = {TPHOLs 2008, LNCS 5170, 33–38},
  year = {2008},
  doi = {10.1007/978-3-540-71067-7\_7},
  url = {https://doi.org/10.1007/978-3-540-71067-7_7}
}
```

- [← previous Soft Syntactic Constraints for Hierarchical Phrased-Based Translation](https://md.research.elamur.ai/free/en/papers/marton-2008-soft-syntactic-constraints-hierarchical-phrased/)
- [next → Labeling Chinese Predicates with Semantic Roles](https://md.research.elamur.ai/free/en/papers/xue-2008-labeling-chinese-predicates-semantic-roles/)
- [↑ back to papers of 2008](https://md.research.elamur.ai/free/en/papers/2008/)

## References

18 references, 0 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Klaus Aehlig and Felix Joachimski. Operational aspects of untyped normalization by evaluation. Mathematical Structures in Computer Science, 14(4):587–611, August 2004. [find](https://scholar.google.com/scholar?q=Klaus+Aehlig+and+Felix+Joachimski%2E+Operational+aspects+of+untyped+normalization+by+evaluation%2E+Mathematical+Structures+in+Computer+Science%2C+14%284%29%3A587%E2%80%93611%2C+August+2004%2E)
2. Bruno Barras. Programming and computing in HOL. In M. Aagaard and J. Harrison, editors, Theorem Proving in Higher Order Logics (TPHOLs 2000), Lecture Notes in Computer Science, pages 17–37. Springer Verlag, 2000. [find](https://scholar.google.com/scholar?q=Bruno+Barras%2E+Programming+and+computing+in+HOL%2E+In+M%2E+Aagaard+and+J%2E+Harrison%2C+editors%2C+Theorem+Proving+in+Higher+Order+Logics+%28TPHOLs+2000%29%2C+Lecture+Notes+in+Computer+Science%2C+pages+17%E2%80%9337%2E+Springer+V)
3. U. Berger, M. Eberl, and H. Schwichtenberg. Term rewriting for normalization by evaluation. Information and Computation, 183:19–42, 2003. [find](https://scholar.google.com/scholar?q=U%2E+Berger%2C+M%2E+Eberl%2C+and+H%2E+Schwichtenberg%2E+Term+rewriting+for+normalization+by+evaluation%2E+Information+and+Computation%2C+183%3A19%E2%80%9342%2C+2003%2E)
4. Ulrich Berger, Matthias Eberl, and Helmut Schwichtenberg. Normalization by evaluation. In B. Möller and J.V. Tucker, editors, Prospects for Hardware Foundations, number 1546 in Lecture Notes in Computer Science, pages 117–137. Springer Verlag, 1998. [find](https://scholar.google.com/scholar?q=Ulrich+Berger%2C+Matthias+Eberl%2C+and+Helmut+Schwichtenberg%2E+Normalization+by+evaluation%2E+In+B%2E+Mo%CC%88ller+and+J%2EV%2E+Tucker%2C+editors%2C+Prospects+for+Hardware+Foundations%2C+number+1546+in+Lecture+Notes+in+Compu)
5. Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed λ–calculus. In R. Vemuri, editor, Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS ’91), pages 203–211, 1991. [find](https://scholar.google.com/scholar?q=Ulrich+Berger+and+Helmut+Schwichtenberg%2E+An+inverse+of+the+evaluation+functional+for+typed+%CE%BB%E2%80%93calculus%2E+In+R%2E+Vemuri%2C+editor%2C+Proceedings+of+the+Sixth+Annual+IEEE+Symposium+on+Logic+in+Computer+Science)
6. N. G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church–Rosser theorem. Indagationes Mathematicae, 34:381–392, 1972. [find](https://scholar.google.com/scholar?q=N%2E+G%2E+de+Bruijn%2E+Lambda+calculus+notation+with+nameless+dummies%2C+a+tool+for+automatic+formula+manipulation%2C+with+application+to+the+Church%E2%80%93Rosser+theorem%2E+Indagationes+Mathematicae%2C+34%3A381%E2%80%93392%2C+1972%2E)
7. Olivier Danvy. Type-directed partial evaluation. In Proceedings of the Twenty-Third Annual ACM SIGPLAN-SIGACT Symposium on Priciples Of Programming Languages (POPL ’96), 1996. [find](https://scholar.google.com/scholar?q=Olivier+Danvy%2E+Type%2Ddirected+partial+evaluation%2E+In+Proceedings+of+the+Twenty%2DThird+Annual+ACM+SIGPLAN%2DSIGACT+Symposium+on+Priciples+Of+Programming+Languages+%28POPL+%E2%80%9996%29%2C+1996%2E)
8. Olivier Danvy, Morten Rhiger, and Christopher H. Rose. Normalisation by evaluation with typed syntax. Journal of Functional Programming, 11(6):673–680, 2001. [find](https://scholar.google.com/scholar?q=Olivier+Danvy%2C+Morten+Rhiger%2C+and+Christopher+H%2E+Rose%2E+Normalisation+by+evaluation+with+typed+syntax%2E+Journal+of+Functional+Programming%2C+11%286%29%3A673%E2%80%93680%2C+2001%2E)
9. Georges Gonthier. A computer-checked proof of the four-colour theorem. [http://research.microsoft.com/](http://research.microsoft.com/) ∼ gonthier/4colproof.pdf. [↗](http://research.microsoft.com/)
10. M.J.C. Gordon and T.F. Melham, editors. Introduction to HOL: a theorem-proving environment for higher order logic. Cambridge University Press, 1993. [find](https://scholar.google.com/scholar?q=M%2EJ%2EC%2E+Gordon+and+T%2EF%2E+Melham%2C+editors%2E+Introduction+to+HOL%3A+a+theorem%2Dproving+environment+for+higher+order+logic%2E+Cambridge+University+Press%2C+1993%2E)
11. Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In International Conference on Functional Programming 2002, pages 235–246. ACM Press, 2002. [find](https://scholar.google.com/scholar?q=Benjamin+Gre%CC%81goire+and+Xavier+Leroy%2E+A+compiled+implementation+of+strong+reduction%2E+In+International+Conference+on+Functional+Programming+2002%2C+pages+235%E2%80%93246%2E+ACM+Press%2C+2002%2E)
12. Florian Haftmann and Tobias Nipkow. A code generator framework for Isabelle/HOL. In Klaus Schneider and Jens Brandt, editors, Theorem Proving in Higher Order Logics: Emerging Trends Proceedings. Department of Computer Science, University of Kaiserslautern, 2007. [find](https://scholar.google.com/scholar?q=Florian+Haftmann+and+Tobias+Nipkow%2E+A+code+generator+framework+for+Isabelle%2FHOL%2E+In+Klaus+Schneider+and+Jens+Brandt%2C+editors%2C+Theorem+Proving+in+Higher+Order+Logics%3A+Emerging+Trends+Proceedings%2E+Depar)
13. Alexander Krauss. Partial recursive functions in higher-order logic. In U. Furbach and N. Shankar, editors, Automated Reasoning (IJCAR 2006), volume 4130 of Lecture Notes in Computer Science, pages 589–603. Springer Verlag, 2006. [find](https://scholar.google.com/scholar?q=Alexander+Krauss%2E+Partial+recursive+functions+in+higher%2Dorder+logic%2E+In+U%2E+Furbach+and+N%2E+Shankar%2C+editors%2C+Automated+Reasoning+%28IJCAR+2006%29%2C+volume+4130+of+Lecture+Notes+in+Computer+Science%2C+pages+58)
14. Tobias Nipkow, Gertrud Bauer, and Paula Schultz. Flyspeck I: Tame graphs. In U. Furbach and N. Shankar, editors, Automated Reasoning (IJCAR 2006), volume 4130 of Lecture Notes in Computer Science, pages 21–35. Springer Verlag, 2006. [find](https://scholar.google.com/scholar?q=Tobias+Nipkow%2C+Gertrud+Bauer%2C+and+Paula+Schultz%2E+Flyspeck+I%3A+Tame+graphs%2E+In+U%2E+Furbach+and+N%2E+Shankar%2C+editors%2C+Automated+Reasoning+%28IJCAR+2006%29%2C+volume+4130+of+Lecture+Notes+in+Computer+Science%2C+pag)
15. Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer Verlag, 2002. [http://www.in.tum.de/](http://www.in.tum.de/) ∼ nipkow/LNCS2283/. [↗](http://www.in.tum.de/)
16. Andrew M. Pitts. Nominal logic, a first order theory of names and binding. Information and Computation, 186:165–193, 2003. [find](https://scholar.google.com/scholar?q=Andrew+M%2E+Pitts%2E+Nominal+logic%2C+a+first+order+theory+of+names+and+binding%2E+Information+and+Computation%2C+186%3A165%E2%80%93193%2C+2003%2E)
17. Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel, and Michael Balser. Structured specifications and interactive proofs with KIV. In W. Bibel and P. Schmitt, editors, Automated Deduction—A Basis for Applications, volume II: Systems and Implementation Techniques, pages 13 – 39. Kluwer, 1998. [find](https://scholar.google.com/scholar?q=Wolfgang+Reif%2C+Gerhard+Schellhorn%2C+Kurt+Stenzel%2C+and+Michael+Balser%2E+Structured+specifications+and+interactive+proofs+with+KIV%2E+In+W%2E+Bibel+and+P%2E+Schmitt%2C+editors%2C+Automated+Deduction%E2%80%94A+Basis+for+App)
18. Christian Urban and Christine Tasson. Nominal techniques in Isabelle/HOL. In Automated Deduction — CADE-20, volume 3632 of Lecture Notes in Computer Science, pages 38–53. Springer Verlag, 2005. [find](https://scholar.google.com/scholar?q=Christian+Urban+and+Christine+Tasson%2E+Nominal+techniques+in+Isabelle%2FHOL%2E+In+Automated+Deduction+%E2%80%94+CADE%2D20%2C+volume+3632+of+Lecture+Notes+in+Computer+Science%2C+pages+38%E2%80%9353%2E+Springer+Verlag%2C+2005%2E)

*Updated 3 November 2026*