natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
A version of type theory.
In practice any type theory is called a simple type theory if type formation is not indexed, that is the judgment that a type $A$ is well-formed has no other inputs. Contrast polymorphic type theory, where types depend on a context of type variables or dependent type theory, where types depend on a context of more general variables.
Original articles:
Bertrand Russell, Mathematical Logic as Based on the Theory of Types, American Journal of Mathematics, Vol. 30, No. 3 (Jul., 1908), pp. 222-262
Alonzo Church, §5 of: A Formulation of the Simple Theory of Types, The Journal of Symbolic Logic 5 2 (1940) 56-68 [doi:10.2307/2266170]
Textbook accounts:
Carl A. Gunter, §2-3 in: Semantics of Programming Languages – Structures and Techniques, MIT Press (1992) [ISBN:9780262570954]
(in a context of programming languages)
See also:
W. Farmer, The seven virtues of simple type theory, Journal of Applied Logic, Vol. 6, No. 3. (September 2008), pp. 267-286.
J. Roger Hindley, Basic Simple Type Theory, Cambridge University Press, 2008
Last revised on January 23, 2023 at 14:35:55. See the history of this page for a list of all contributions to it.