Computational type theory is a semantic formulation of dependent type theory that starts with a programming language equipped with a deterministic operational semantics and derives types as specifications of program behavior. Thus, a type is a program specification, two types are exactly equal only if they specify the same behavior, and a program inhabits a type if it behaves according to specification, and two programs are exactly equal as elements of a type when they exhibit the same specified behavior. The range of possible programs is open-ended in that no specification precludes the existence of any program, and the forms of type that may be considered are unlimited, the presence of one type never interfering with another. Among the types are those arising from logic, including the usual connectives and quantifiers. From the logical perspective computational type theory is a theory of truth, not a theory of formal proof, thereby providing a direct realization of Brouwer’s program of intuitionistic foundations for mathematics. The role of formalisms is strictly secondary, and never imposes definitional limits on the theory. Whereas computational type theory is consistent with the familiar constructs of formal type theory, it is both possible and advantageous to consider proof theories, such as refinement logics, that lie outside the scope of formal type theory. As mentioned, computational type theory has its roots in Brouwer’s program of intuitionistic mathematics in which the truth of a proposition is identified with the existence of a construction (program) that obeys the proposition as a specification. This perspective was developed by Martin-Loef in his paper “Constructive Mathematics and Computer Programming”, and was developed more fully by Constable and his co-workers in the NuPRL type theory and proof assistant. More recently, computational type theory has been extended by the authors to account for higher-dimensional phenomena (as suggested by Hofmann, Streicher, Moerdijk, Berg, Warren, Awodey, and Voevodsky), such as the identification of equivalent types, or the formation of abstract higher-dimensional objects in type theory.

The purpose of this tutorial is to present the semantics of computational higher type theory, and to relate the semantics to its implementation in the RedPRL proof development system.