Elamur Research⌕
☰
home / papers / 2008 / The Isabelle Framework

The Isabelle Framework

Paper · 2008 · Makarius Wenzel, Lawrence C. Paulson and Tobias Nipkow

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 CambridgeCambridge · United Kingdom287 works · 125,174 citations🎓Technical University of MunichMunich · Germany66 works · 49,493 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.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. DOI 10.1007/978-3-540-71067-7_7

@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}
}

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
  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
  3. U. Berger, M. Eberl, and H. Schwichtenberg. Term rewriting for normalization by evaluation. Information and Computation, 183:19–42, 2003. find
  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
  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
  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
  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
  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
  9. Georges Gonthier. A computer-checked proof of the four-colour theorem. http://research.microsoft.com/ ∼ gonthier/4colproof.pdf. ↗
  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
  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
  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
  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
  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
  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/ ∼ nipkow/LNCS2283/. ↗
  16. Andrew M. Pitts. Nominal logic, a first order theory of names and binding. Information and Computation, 186:165–193, 2003. find
  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
  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

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/wenzel-2008-isabelle-framework/