SIMPLE TYPE THEORY IN EVES

Authors
  1. Saaltink, M.
  2. Craigen, D.
Corporate Authors
Odyssey Research Associates Inc, Ottawa ONT (CAN);Chief of Research and Development, Ottawa ONT (CAN) Director of Research and Development Communications and Space
Abstract
The 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.
Date of publication
01 Jan 1990
Number of Pages
27
DSTKIM No
91-00745
CANDIS No
67962
Format(s):
Hardcopy;Originator's fiche received by DSIS

Permanent link

Document 1 of 1

Date modified: