| Programming in Martin-Lof Type Theory Unification A non-trivial Example (1999) | |||||||||||||
Abstract | |||||||||||||
| Martin-Lof's type theory is a constructive type theory originally conceived as a formal language in which to carry out constructive mathematics. However, it can also be viewed as a programming language where specifications are represented as types and programs as objects of the types. In this work, the use of type theory as a programming language is investigated. As an example, a formalisation of a unification algorithm for first-order terms is considered. Unification can be seen as the process of finding a substitution that makes all the pairs of terms in an input list equal, if such a substitution exists. Unification algorithms are crucial in many applications, such as type checkers for different programming languages. Unification algorithms are total and recursive, but the arguments on which the recursive calls are performed satisfy no syntactic condition that guarantees termination. This fact is of great importance when working with Martin-Lof's type theory since there is no direc... | |||||||||||||
Details der Publikation | |||||||||||||
| |||||||||||||