Advertisement

Simple Type Theory in EVES

  • Mark Saaltink
  • Dan Craigen
Conference paper
Part of the Workshops in Computing book series (WORKSHOPS COMP.)

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.

Keywords

Type Theory Abstract Syntax Verification System Proof Obligation Initial Theory 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: to Truth through Proof. Academic Press, 1986.Google Scholar
  2. [2]
    Dan Craigen. A Description of m-Verdi. IPSA Technical Report TR-87–542002, November, 1987.Google Scholar
  3. [3]
    Dan Craigen, et al. M-EVES: A Tool for Verifying Software, in Proc. of 10th International Conference on Software Engineering, April 1988, Singapore.Google Scholar
  4. [4]
    Dan Craigen. Reference Manual for the Language Verdi,ORA Technical Report TR–90–5429–09, February 1990.Google Scholar
  5. [5]
    Dan Craigen. An Application of the m-EVES Verification System. 2nd Workshop on Software Testing, Verification and Analysis (July 1988), Banff, Alberta.Google Scholar
  6. [6]
    H. B. Curry and R. Feys. Combinatory Logic, Vol. 1. North Holland, 1958Google Scholar
  7. [7]
    Friedrich von Henke, Natarajan Shankar, John Rushby. Formal Semantics of EHDM. Technical Report, Computer Science Laboratory, SRI International, January 1990.Google Scholar
  8. [9]
    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.Google Scholar
  9. [10]
    Paul R. Halmos. Naive Set Theory. Van Nostrand, 1960.Google Scholar
  10. [11]
    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.Google Scholar
  11. [12]
    Sentot Kromodimoeljo and Bill Pase. Using the EVES Library Facility: A PICO Interpreter. ORA Technical Report TR–90–5444–02, February 1990.Google Scholar
  12. [13]
    Irwin Meisels. TR Program Example. ORA Technical Report TR–89–5443–02, August 1989.Google Scholar
  13. [14]
    Irwin Meisels. WC Program Example. ORA Technical Report TR–89–5443–03, October 1989.Google Scholar
  14. [15]
    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.Google Scholar
  15. [16]
    Luis Elpidio Sanchis. Functionals Defined by Recursion, in the Notre Dame Journal of Formal Logic 8(3): 161–174, July 1967.CrossRefMathSciNetGoogle Scholar
  16. [17]
    Mark Saaltink. The Mathematics of m–Verdi. I.P. Sharp Technical Report FR–87–5420–03, November 1987.Google Scholar
  17. [18]
    Mark Saaltink. A Formal Description of Verdi. ORA Technical Report TR-895429–10, October 1989.Google Scholar
  18. [19]
    Mark Saaltink. The Mechanical Verification of a Simple Control System. ORA Technical Report TR–89–5443–04, December 1989.Google Scholar
  19. [20]
    D. A. Turner. Another Algorithm for Bracket Abstraction, in the Journal of Symbolic Logic 44(2): 267–270, June 1979.Google Scholar

Copyright information

© British Computer Society 1991

Authors and Affiliations

  • Mark Saaltink
    • 1
  • Dan Craigen
    • 1
  1. 1.Odyssey Research AssociatesOttawaCanada

Personalised recommendations