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 (10)

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

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