The seven virtues of simple type theory

DOI10.1016/J.JAL.2007.11.001zbMATH Open1149.03012OpenAlexW2097181978MaRDI QIDQ946569FDOQ946569

Authors: William M. Farmer 

Publication date: 23 September 2008

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

Full work available at URL: https://doi.org/10.1016/j.jal.2007.11.001

Recommendations

• Simple Type Theory
• Classical type theory
• scientific article; zbMATH DE number 559219
• A simple type theory without Platonic domains
• A simple type theory with partial functions and subtypes

zbMATH Keywords

surveyPeano arithmetictype theoryhigher-order logicnonstandard modelscomplete ordered fieldpractical logics

Mathematics Subject Classification ID

Cites Work

• An introduction to mathematical logic and type theory: To truth through proof.
• Title not available (Why is that?)
• IMPS: An interactive mathematical proof system
• Edinburgh LCF. A mechanized logic of computation
• Title not available (Why is that?)
• Isabelle. A generic theorem prover
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The completeness of the first-order functional calculus
• The B-Book
• TPS: A theorem-proving system for classical type theory
• Completeness in the theory of types
• The calculus of constructions
• A simple type theory with partial functions and subtypes
• Automated Reasoning
• The strength of Mac Lane set theory
• A theory of prepositional types
• On the consistency of a slight (?) modification of Quine's 'New Foundations'
• The Discovery of My Completeness Proofs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• A reduction of the axioms for the theory of prepositional types
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A mechanization of strong Kleene logic for partial functions
• A partial functions version of Church's simple theory of types
• Practical forms of type theory

Cited In (15)

• Probabilistic modelling, inference and learning using logical theories
• Probabilities on sentences in an expressive logic
• On the number of types
• PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
• Incorporating quotation and evaluation into Church's type theory
• Elements of model theory in higher-order fuzzy logic
• Title not available (Why is that?)
• In the Search of a Naive Type Theory
• Shallow embedding of type theory is morally correct
• Higher-order concepts for the potential infinite
• Combining logics in simple type theory
• Terminating tableau systems for hybrid logic with difference and converse
• A simple type theory without Platonic domains
• Towards a symbolic approach to sound analysis
• Simple Type Theory

Uses Software

• Coq
• Isabelle
• TPS
• ML
• PVS
• HOL
• ETPS
• Nuprl
• IMPS
• LEGO
• Z

This page was built for publication: The seven virtues of simple type theory

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