Abstract
This article describes a set of derived inference rules and an abstract reduction machine using them that allow the inplementation of an interpreter for HOL terms, with the same complexity as with ML code. The latter fact allows us to use HOL as a computer algebra system in which the user can implement algorithms, provided he proved them correct.
This is a preview of subscription content, log in via an institution to check access.
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
M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, pages 31–46. ACM, January 1990. Also Digital Equipment Corporation, Systems Research Center, Research Report 54, February 1990.
H. Barendregt. Lambda Calculi with Types. Technical Report 91-19, Catholic University Nijmegen, 1991. In Handbook of Logic in Computer Science, Vol II.
B. Barras. Auto-validation d’un système de preuves avec familles inductives. Thèse de doctorat, Université Paris 7, November 1999.
B. Barras, S. Boutin, C. Cornes, J. Courant, J.-C. Filliâtre, E. Giménez, H. Herbelin, G. Huet, C. Muñoz, C. Murthy, C. Parent, C. Paulin, A. Saïbi, and B. Werner. The Coq Proof Assistant Reference Manual version 6.1. Technical Report 0203, Projet Coq-INRIA Rocquencourt-ENS Lyon, August 1997.
R.J. Boulton. Lazy techniques for fully expansive theorem proving. Formal Methods in System Design, 3(1/2):25–47, August 1993.
S. Boutin. Using reflection to build efficient and certified decision procedures. In Martin Abadi and Takahashi Ito, editors, TACS’97, volume 1281. LNCS, Springer-Verlag, 1997.
P. Crégut. An abstract machine for λ-terms normalization. In Gilles Kahn, editor, Proceedings of the ACM Conference on LISP and Functional Programming, pages 333–340, Nice, France, June 1990. ACM Press.
Pierre-Louis Curien, Thérèse Hardin, and Jean-Jacques Levy. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43(2):362–397, March 1996.
N.J. De Bruijn. Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indag. Math., 34(5), pp. 381–392, 1972.
M. J. C. Gordon and T. F. Melham. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.
M. J. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF. LNCS 78. Springer-Verlag, 1979.
P.-A. Melliès. Typed λ-calculi with explicit substitutions may not terminate. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, Edinburgh, Scotland, April 1995. Springer-Verlag LNCS 902.
Lawrence C. Paulson. A higher-order implementation of rewriting. Science of Computer Programming, 3:119–149, 1983.
Lawrence C. Paulson. Logic and Computation: Interactive proof with Cambridge LCF. Cambridge University Press, 1987.
K. Slind. Function definition in higher order logic. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, Turku, Finland, volume 1125, pages 381–397. LNCS, Springer-Verlag, August 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barras, B. (2000). Programming and Computing in HOL. In: Aagaard, M., Harrison, J. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2000. Lecture Notes in Computer Science, vol 1869. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44659-1_2
Download citation
DOI: https://doi.org/10.1007/3-540-44659-1_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67863-2
Online ISBN: 978-3-540-44659-0
eBook Packages: Springer Book Archive