Simple type theory is formulated for use with the genertic theorem prover Isabelle. This requires explicit type inference rules. There are function, product, and subset types, which may be empty. Descriptions (the η-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.
CITATION STYLE
Paulson, L. C. (1990). A formulation of the simple theory of types (For Isabelle). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 417 LNCS, pp. 246–274). Springer Verlag. https://doi.org/10.1007/3-540-52335-9_58
Mendeley helps you to discover research relevant for your work.