A simple type theory with partial functions and subtypes

DOI10.1016/0168-0072(93)90144-3MaRDI QIDQ1314643zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• A partial functions version of Church's simple theory of types
• Automated Deduction – CADE-19
• Partial functions in type theory
• scientific article; zbMATH DE number 1341476
• HYBRID PARTIAL-TOTAL TYPE THEORY

Cites work

• scientific article; zbMATH DE number 3467028 (Why is no real title available?)
• scientific article; zbMATH DE number 3550662 (Why is no real title available?)
• scientific article; zbMATH DE number 3999882 (Why is no real title available?)
• scientific article; zbMATH DE number 3248792 (Why is no real title available?)
• A partial functions version of Church's simple theory of types
• A reduction of the axioms for the theory of prepositional types
• A theory of prepositional types
• Automated deduction -- CADE-11. Proceedings of the 11th international conference held in Saratoga Springs, NY, USA, June 15--18, 1992
• Completeness in the theory of types

Cited in

(16)

• The seven virtues of simple type theory
• Incorporating quotation and evaluation into Church's type theory
• Andrews' type theory with undefinedness
• HYBRID PARTIAL-TOTAL TYPE THEORY
• Subtypes in fuzzy type theory
• A set theory with support for partial functions
• Partiality and recursion in interactive theorem provers -- an overview
• A two-valued logic for properties of strict functional programs allowing partial functions
• Automated Deduction – CADE-19
• In the Search of a Naive Type Theory
• scientific article; zbMATH DE number 2003151 (Why is no real title available?)
• IMPS: An interactive mathematical proof system
• A simple type theory without Platonic domains
• IMPS: An updated system description
• A partial functions version of Church's simple theory of types
• Simple Types in Type Theory: Deep and Shallow Encodings

Describes a project that uses

Uses Software

• IMPS
• ETPS

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1314643)