A simple type theory with partial functions and subtypes

DOI10.1016/0168-0072(93)90144-3zbMath0837.03003OpenAlexW2316406086MaRDI QIDQ1314643

William M. Farmer

Publication date: 13 May 1996

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0168-0072(93)90144-3

zbMATH Keywords

simple type theoryaxiomatic systemsubtypesfoundation for mechanized mathematicsHenkin-style general models semanticsinteractive mathematical proof system

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (7)

A two-valued logic for properties of strict functional programs allowing partial functions ⋮ In the Search of a Naive Type Theory ⋮ The seven virtues of simple type theory ⋮ IMPS: An updated system description ⋮ Incorporating quotation and evaluation into Church's type theory ⋮ Partiality and recursion in interactive theorem provers – an overview ⋮ Subtypes in fuzzy type theory

Uses Software

• ETPS
• IMPS

Cites Work

• Automated deduction -- CADE-11. Proceedings of the 11th international conference held in Saratoga Springs, NY, USA, June 15--18, 1992
• A theory of prepositional types
• A reduction of the axioms for the theory of prepositional types
• A partial functions version of Church's simple theory of types
• Completeness in the theory of types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A simple type theory with partial functions and subtypes