The elements of propositions, when interpreted as types, are called proof-objects. When proof-objects are added to the natural deduction calculus it becomes a typed lambda calculus with dependent types, which extends Church’s original typed lambda calculus. The equality rules are computation rules for the terms of this calculus. Each function definable in the theory is total and computable. Intuitionistic type theory is thus a typed functional programming language with the unusual property that all programs terminate.