J.-C. Filliātre. Proof of Imperative Programs in Type Theory. In International Workshop, TYPES '98, Kloster Irsee, Germany, volume 1657 of Lecture Notes in Computer Science. Springer-Verlag, March 1998.

We present a new approach to certifying imperative programs, in the context of Type Theory. The key is a functional translation of imperative programs, which is made possible by an analysis of their effects. On sequential imperative programs, we get the same proof obligations as those given by Floyd-Hoare logic, but our approach also includes functional constructions. As a side-effect, we propose a way to eradicate the use of auxiliary variables in specifications. This work has been implemented in the Coq Proof Assistant and applied on non-trivial examples.

[ bib | .ps.gz ]

Back