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
Originally, “simple type theory” was the name of the type theory introduced by Church (1940) (therefore often and more informatively: “Church’s type theory” or similar). This type theory allowed (only) function type-type formation (therefore often: “simply typed lambda-calculus”) based on two elementary types (a kind of type of natural numbers and a type of propositions).
In mild generalization, if one admits in addition product type-type formation then [e.g. Gunter (1992)] these are the type theories whose categorical semantics is in cartesian closed categories (see also at relation between category theory and type theory).
More generally, the term “simple type theory” has come to refer to any type theory whose type formations are not indexed, in that the judgment that a type is well-formed has no other inputs, understood in contrast to:
polymorphic type theory, where types depend on a context of type variables,
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]
See also
Lecture notes:
Textbook accounts:
J. Roger Hindley, Basic Simple Type Theory, Cambridge University Press (1997, 2009) [doi:10.1017/CBO9780511608865]
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:
Last revised on February 28, 2023 at 14:35:38. See the history of this page for a list of all contributions to it.