References & Citations
Computer Science > Logic in Computer Science
Title: A Formulation of the Simple Theory of Types (for Isabelle)
(Submitted on 31 Oct 2000)
Abstract: Simple type theory is formulated for use with the generic theorem prover Isabelle. This requires explicit type inference rules. There are function, product, and subset types, which may be empty. Descriptions (the eta-operator) introduce the Axiom of Choice. Higher-order logic is obtained through reflection between formulae and terms of type bool. Recursive types and functions can be formally constructed. Isabelle proof procedures are described. The logic appears suitable for general mathematics as well as computational problems.
Link back to: arXiv, form interface, contact.