Thumbnail
Access Restriction
Open

Author Bove, Ana
Source CiteSeerX
Content type Text
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Different Programming Language ♦ Constructive Mathematics ♦ Formal Language ♦ Great Importance ♦ Type Checker ♦ Many Application ♦ Recursive Call ♦ Unification Algorithm ♦ First-order Term ♦ Programming Language ♦ Input List ♦ Type Theory ♦ Constructive Type Theory ♦ Syntactic Condition
Description Martin-Löf'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-Löf's type theory since there is no direc...
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article
Publisher Date 1999-01-01
Publisher Department Department of Computer Science, Chalmers University of Technology