IJPAM: Volume 42, No. 4 (2008)
AUTOMATED PROGRAM WRITING
Empire State College
State University of New York
325 Hudson Street, New York, NY 10013, USA
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