Abstract
This paper presents a brief description of a newly completed verification system called EVES. EVES is a formal system based on Zermelo-Fraenkel set theory with the Axiom of Choice. EVES supports the proof of mathematical properties, including proofs of program correctness. The development of EVES required the design of a new language, called Verdi, and of a heuristic theorem prover, called NEVER.
After introductory remarks on Verdi, NEVER and EVES, we present a combinatory version of Church’s simple type theory in EVES as an illustration of the power and flexibility of the untyped set theory framework and of EVES.
The development of EVES was sponsored by the Canadian Department of National Defence through DSS contract W2207-8-AF78/01SV.
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
Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: to Truth through Proof. Academic Press, 1986.
Dan Craigen. A Description of m-Verdi. IPSA Technical Report TR-87–542002, November, 1987.
Dan Craigen, et al. M-EVES: A Tool for Verifying Software, in Proc. of 10th International Conference on Software Engineering, April 1988, Singapore.
Dan Craigen. Reference Manual for the Language Verdi,ORA Technical Report TR–90–5429–09, February 1990.
Dan Craigen. An Application of the m-EVES Verification System. 2nd Workshop on Software Testing, Verification and Analysis (July 1988), Banff, Alberta.
H. B. Curry and R. Feys. Combinatory Logic, Vol. 1. North Holland, 1958
Friedrich von Henke, Natarajan Shankar, John Rushby. Formal Semantics of EHDM. Technical Report, Computer Science Laboratory, SRI International, January 1990.
Mike Gordon. HOL: A Proof Generating System for Higher-Order Logic. in VLSI Specification, Verification and Synthesis, G. Birtwistle and P.A. Subrahmanyan (eds), Kluwer 1987.
Paul R. Halmos. Naive Set Theory. Van Nostrand, 1960.
Keith Hanna. VERITAS+, A Specification Language based on Type Theory, in Proc. of Workshop on Hardware Verification, Verification and Synthesis: Mathematical Aspects,Cornell University, 1989, M. Leeser and G. Brown (eds), Lecture Notes in Computer Science, Vol. 408, Springer-Verlag.
Sentot Kromodimoeljo and Bill Pase. Using the EVES Library Facility: A PICO Interpreter. ORA Technical Report TR–90–5444–02, February 1990.
Irwin Meisels. TR Program Example. ORA Technical Report TR–89–5443–02, August 1989.
Irwin Meisels. WC Program Example. ORA Technical Report TR–89–5443–03, October 1989.
Bill Pase and Mark Saaltink. Formal Verification in m-EVES, in Current Trends in Hardware Verification and Automated Theorem Proving, G. Birtwistle and P.A. Subrahmanyam (eds), Springer-Verlag, 1989.
Luis Elpidio Sanchis. Functionals Defined by Recursion, in the Notre Dame Journal of Formal Logic 8(3): 161–174, July 1967.
Mark Saaltink. The Mathematics of m–Verdi. I.P. Sharp Technical Report FR–87–5420–03, November 1987.
Mark Saaltink. A Formal Description of Verdi. ORA Technical Report TR-895429–10, October 1989.
Mark Saaltink. The Mechanical Verification of a Simple Control System. ORA Technical Report TR–89–5443–04, December 1989.
D. A. Turner. Another Algorithm for Bracket Abstraction, in the Journal of Symbolic Logic 44(2): 267–270, June 1979.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1991 British Computer Society
About this paper
Cite this paper
Saaltink, M., Craigen, D. (1991). Simple Type Theory in EVES. In: Birtwistle, G. (eds) IV Higher Order Workshop, Banff 1990. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3182-3_13
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3182-3_13
Publisher Name: Springer, London
Print ISBN: 978-3-540-19660-0
Online ISBN: 978-1-4471-3182-3
eBook Packages: Springer Book Archive