Abstract
We present a novel compiled approach to Normalization by Evaluation (NBE) for ML-like languages. It supports efficient normalization of open λ-terms w.r.t. β-reduction and rewrite rules. We have implemented NBE and show both a detailed formal model of our implementation and its verification in Isabelle. Finally we discuss how NBE is turned into a proof rule in Isabelle.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aehlig, K., Joachimski, F.: Operational aspects of untyped normalization by evaluation. Mathematical Structures in Computer Science 14(4), 587–611 (2004)
Barras, B.: Programming and computing in HOL. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 17–37. Springer, Heidelberg (2000)
Berger, U., Eberl, M., Schwichtenberg, H.: Term rewriting for normalization by evaluation. Information and Computation 183, 19–42 (2003)
Berger, U., Eberl, M., Schwichtenberg, H.: Normalization by evaluation. In: Möller, B., Tucker, J.V. (eds.) NADA 1997. LNCS, vol. 1546, pp. 117–137. Springer, Heidelberg (1998)
Berger, U., Schwichtenberg, H.: An inverse of the evaluation functional for typed λ–calculus. In: Vemuri, R. (ed.) Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS 1991), pp. 203–211 (1991)
de Bruijn, N.G.: 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)
Danvy, O.: Type-directed partial evaluation. In: Proceedings of the Twenty-Third Annual ACM SIGPLAN-SIGACT Symposium on Priciples Of Programming Languages (POPL 1996) (1996)
Danvy, O., Rhiger, M., Rose, C.H.: Normalisation by evaluation with typed syntax. Journal of Functional Programming 11(6), 673–680 (2001)
Gonthier, G.: A computer-checked proof of the four-colour theorem, http://research.microsoft.com/~gonthier/4colproof.pdf
Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: a theorem-proving environment for higher order logic. Cambridge University Press, Cambridge (1993)
Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: International Conference on Functional Programming 2002, pp. 235–246. ACM Press, New York (2002)
Haftmann, F., Nipkow, T.: A code generator framework for Isabelle/HOL. In: Schneider, K., Brandt, J. (eds.) Theorem Proving in Higher Order Logics: Emerging Trends Proceedings. Department of Computer Science, University of Kaiserslautern (2007)
Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 589–603. Springer, Heidelberg (2006)
Nipkow, T., Bauer, G., Schultz, P.: Flyspeck I: Tame graphs. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 21–35. Springer, Heidelberg (2006)
Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002), http://www.in.tum.de/~nipkow/LNCS2283/
Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation 186, 165–193 (2003)
Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: tructured specifications and interactive proofs with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction—A Basis for Applications. Systems and Implementation Techniques, vol. II, pp. 13–39. Kluwer Academic Publishers, Dordrecht (1998)
Urban, C., Tasson, C.: Nominal techniques in Isabelle/HOL. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 38–53. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aehlig, K., Haftmann, F., Nipkow, T. (2008). A Compiled Implementation of Normalization by Evaluation. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2008. Lecture Notes in Computer Science, vol 5170. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71067-7_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-71067-7_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71065-3
Online ISBN: 978-3-540-71067-7
eBook Packages: Computer ScienceComputer Science (R0)