Abstract.In [#!ml1!#] and [#!ml2!#] Per Martin-Löf has introduced his type theory. Any problem defined in the ``language" of type theory is a type in that theory. To solve the problem, that is, to infer (deduce) the type that represents the problem in the theory is the same as to construct an object of that type. Based on the construction of that object, a program can be created that produces a solution of the problem. The automation of the above mentioned procedures will result in a system for automated program writing. To achieve this goal first the theoretical basis should be established. It requires a large number of scholastic proofs and results. The most important result is consistency of the theory. I have proved the consistency of Martin-Löf's type theory. In January 2006 it was submitted for publication in Springer Archive for Mathematical Logic.

In this article I describe Martin-Löf's type theory (MLTT) for automated program writing. MLTT is based on Martin Löf's type theory presented in [#!ml1!#] and [#!ml2!#].

Received: August 17, 2007

AMS Subject Classification: 03A68

Key Words and Phrases: Martin-Löf's type theory, automated program writing, automated problem solving

Source: International Journal of Pure and Applied Mathematics
ISSN: 1311-8080
Year: 2008
Volume: 42
Issue: 4