A simple type theory with partial functions and subtypes

DOI10.1016/0168-0072(93)90144-3zbMATH Open0837.03003OpenAlexW2316406086MaRDI QIDQ1314643FDOQ1314643

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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Completeness in the theory of types
• Title not available (Why is that?)
• 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
• A reduction of the axioms for the theory of prepositional types
• A partial functions version of Church's simple 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
• Automated Deduction – CADE-19
• A two-valued logic for properties of strict functional programs allowing partial functions
• In the Search of a Naive Type Theory
• Title not available (Why is that?)
• 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

Uses Software

• ETPS
• IMPS

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)