The seven virtues of simple type theory

DOI10.1016/J.JAL.2007.11.001MaRDI QIDQ946569zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

surveyPeano arithmetictype theoryhigher-order logicnonstandard modelscomplete ordered fieldpractical logics

Mathematics Subject Classification ID

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

Cites work

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

Cited in

(15)

• Simple Type Theory
• 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
• scientific article; zbMATH DE number 3999882 (Why is no real title available?)
• 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

Describes a project that uses

Uses Software

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

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)