Building new constructive logical systems ⋆

Abstract. Curry and and Howard observed that ordinary propositional logic can also be viewed as a functional (programming) language. Thus programs are contained, in a certain sense, in proofs in mathematical logic. This has led to the viewing of proofs (originally, just in formal logic) as computer programs. The advantage of these techniques is that the task of programming a function is reduced to reasoning with domain knowledge. In this paper we look at extensions of the Curry-Howard correspondence into an application: algebraic specifications using the language Casl. The full details may be found in our forthcoming book with Iman Poernomo and Martin Wirsing. We also take a more abstract view of the process in which we are engaged and how one can incorporate other ideas, such as those of context and state, into the logic.