Abstract
Finite maps, functions defined on only a finite domain, occur often, particularly when reasoning about programming languages. This paper presents a theory of finite maps in HOL. We discuss the choice of representation, present the theory we have defined, and discuss the issue of defining recursive types containing finite maps. We also discuss decision procedures and give an example of the use of finite maps in developing the semantics of a small language.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.
M.J.C. Gordon. Merging HOL with Set Theory: preliminary experiments. Technical Report 353, University of Cambridge Computer Laboratory, 1994.
Elsa Gunter. A Broader Class of Trees for Recursive Type Definitions for HOL. In J. J. Joyce and C. J. H. Seger, editors, Higher Order Logic Theorem Proving and its Applications, volume 780 of Lecture Notes in Computer Science, pages 141–154. Springer-Verlag, 1993.
Savi Maharaj and Elsa Gunter. Studying the ML Module System in HOL. In Tom Melham and Juanito Camilleri, editors, Higher Order Logic Theorem Proving and its Applications, volume 859 of Lecture Notes in Computer Science. Springer-Verlag, September 1994.
Tom F. Melham. Recursive Data Types. Message on info-hol mailing list, 9th November 1991.
Tom F. Melham. Automating Recursive Type Definitions in HOL. In Graham Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 341–386. Springer-Verlag, 1989.
Tom F. Melham. A Package for Inductive Relation Definitions in HOL. In M. Archer, J J Joyce, K N Levitt, and P J Windley, editors, Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, Davis, August 1992, pages 350–357. IEEE Computer Society Press, 1992.
Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. The MIT Press, 1990.
Donald Syme. Reasoning with the Formal Definition of Standard ML in HOL. In Higher Order Logic Theorem Proving and Its Applications, volume 780 of Lecture Notes in Computer Science, pages 43–60. Springer-Verlag.
Donald Syme. Supporting Formal Reasoning about Standard ML. Honours Thesis, Australian National University, 1992.
Myra VanInwegen and Elsa Gunter. HOL-ML. In J. J. Joyce and C. J. H. Seger, editors, Higher Order Logic Theorem Proving and its Applications, volume 780 of Lecture Notes in Computer Science, pages 61–74. Springer-Verlag, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Collins, G., Syme, D. (1995). A theory of finite maps. In: Thomas Schubert, E., Windley, P.J., Alves-Foss, J. (eds) Higher Order Logic Theorem Proving and Its Applications. TPHOLs 1995. Lecture Notes in Computer Science, vol 971. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60275-5_61
Download citation
DOI: https://doi.org/10.1007/3-540-60275-5_61
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60275-0
Online ISBN: 978-3-540-44784-9
eBook Packages: Springer Book Archive