The seven virtues of simple type theory
type: Item
instance of: scholarly article
title: The seven virtues of simple type theory
zbMATH Open document ID: 1149.03012
author: William M. Farmer
published in: Journal of Applied Logic
publication date: 2008-09-23T00:00:00Z
Mathematics Subject Classification ID: 03B15
zbMATH DE Number: 5346254
zbMATH Keywords: higher-order logic
zbMATH Keywords: type theory
zbMATH Keywords: practical logics
zbMATH Keywords: nonstandard models
zbMATH Keywords: Peano arithmetic
zbMATH Keywords: complete ordered field
zbMATH Keywords: survey
describes a project that uses: Coq
describes a project that uses: Isabelle
describes a project that uses: TPS
describes a project that uses: PVS
describes a project that uses: ETPS
describes a project that uses: ML
describes a project that uses: IMPS
describes a project that uses: Z
describes a project that uses: HOL
describes a project that uses: Nuprl
describes a project that uses: LEGO
MaRDI profile type: Publication
full work available at URL: j.jal.2007.11.001
OpenAlex ID: W2097181978
cites work: The B-Book
cites work: A reduction of the axioms for the theory of prepositional types
cites work: An introduction to mathematical logic and type theory: To truth through proof.
cites work: TPS: A theorem-proving system for classical type theory
cites work: The calculus of constructions
cites work: A partial functions version of Church's simple theory of types
cites work: A simple type theory with partial functions and subtypes
cites work: Automated Reasoning
cites work: IMPS: An interactive mathematical proof system
cites work: Q4674788
cites work: Q3875893
cites work: Q3994895
cites work: Q5287513
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: Q4342091
cites work: The completeness of the first-order functional calculus
cites work: Completeness in the theory of types
cites work: A theory of prepositional types
cites work: The Discovery of My Completeness Proofs
cites work: Q4281475
cites work: On the consistency of a slight (?) modification of Quine's 'New Foundations'
cites work: Q4012178
cites work: A mechanization of strong Kleene logic for partial functions
cites work: Q3727946
cites work: Q4692751
cites work: Q3688389
cites work: The strength of Mac Lane set theory
cites work: Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
cites work: Isabelle. A generic theorem prover
cites work: Q3995087
cites work: Practical forms of type theory
DOI: 10.1016/J.JAL.2007.11.001
description: scientific article; zbMATH DE number 5346254