Proof of Imperative Programs in Type Theory

Proofs of correctness of imperative programs are traditionally done in first order frameworks derived from Hoare logic [8]. On the other hand, correctness proofs of purely functional programs are almost always done in higher order logics. In particular, the realizability [10] allow to extract correct functional programs from constructive proofs of existential formulae. In this paper, we establish a relation between these two approaches and show how proofs in Hoare logic can be interpreted in type theory, yielding a translation of imperative programs into functional ones. Starting from this idea, we proposeaninterpretation of correctness formulae in type theory for a programming language mixing imperative and functional features. One consequence is a good and natural solution to the problems of procedures and side-effects in expressions