Normalising the associative law: An experiment with Martin-Löf's type theory

Abstract

Martin-Löf's type theory contains a logic, a specification language and a programming language, so it is a tool with different uses. Although it is traditionally used as an integrated programming logic, it may well be used as an external logic, which is necessary if one wants to use the formalism of type theory to verify the correctness of an external program. Different tools, such as well founded recursion, measure functions, or the separation of correctness into termination and partial correctness, may be used to obtain a correct type theory program. Type theory is viewed as an open system with respect to inductively defined types and predicates, which makes it easy to represent an external program as a graph. Formal proofs have been edited using Larry Paulson's ISABELLE. © 1991 BCS.