Logics for Termination and Correctness of Functional Programs

In the literature of logic and theoretical computer science, types are considered both semantically as some kinds of mathematical objects and syntactically as certain kinds of formal terms. They are dealt with in one way or the other, or both, in all programming languages, though most attention has been given to their role in functional programming languages. One difference in treatment lies in the extent to which types are explicitly represented in programs themselves and, further, can be passed as values. Familiar examples, more or less at the extremes, are provided by LISP—an untyped language— and ML—a polymorphic typed language. The aim of this paper (and the more detailed ones to follow) is to provide a logical foundation for the use of type systems in functional programming languages and to set up logics for the termination and correctness of programs relative to such systems. The foundation provided here includes LISP and ML as special cases. I believe this work should be adaptable to other kinds of programming languages, e.g. those of imperative style.