The seven virtues of simple type theory

DOI10.1016/j.jal.2007.11.001zbMath1149.03012OpenAlexW2097181978MaRDI QIDQ946569

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

zbMATH Keywords

surveyhigher-order logicnonstandard modelsPeano arithmetictype theorycomplete ordered fieldpractical logics

Mathematics Subject Classification ID

Related Items

Probabilistic modelling, inference and learning using logical theories, Towards a Symbolic Approach to Sound Analysis, In the Search of a Naive Type Theory, Higher-order concepts for the potential infinite, On the number of types, Probabilities on sentences in an expressive logic, Incorporating quotation and evaluation into Church's type theory, Elements of model theory in higher-order fuzzy logic, PNL to HOL: from the logic of nominal sets to the logic of higher-order functions, Terminating tableau systems for hybrid logic with difference and converse

Uses Software

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

Cites Work

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