Abstract

The paper begins with a discussion of type theory. This is the logical system in which the proofs-as-programs paradigm will be explored. We could have used a simpler logic such as higher-order number theory. But the amount of work involved in explaining that theory is not appreciably less than what we will do here, and it is one of my secondary goals to present the elements of constructive type theory. So the details of how the type theory is presented will be of independent interest. The next section discusses programming in type theory. We will see that the programming part looks a lot like a functional programming language with rich types such as Standard ML [20, 24]; already at this point we can appreciate the value of using type theory as opposed to other formalisms.

In section 4 we examine how logic is defined on top of the type theory. Here we invoke 3 the well-known propositions-as-types principle, and we define the sublogics of construc- tive and classical arithmetic (so-called Heyting and Peano arithmetics respectively). In section 5 we examine program derivation from specification. Then in section 6 we expand the programming language to include the control operators of Felliesen [12]. This is the programming basis for the extension of the logic in section 7 to interpret classical proofs computationally.