Programming with Effects in Coq

Next-generation programming languages will move beyond simple type systems to include support for formal specifications and mechanically- checked proofs of adherence to those requirements. Already, in the imperative world, languages such as

ESC/Java

and

Spec

# integrate Hoare- style pre- and post-conditions into the underlying type system. However, we argue that neither the program logics used in these systems, nor the decision procedures used to discharge verification conditions, are sufficient for establishing deep properties of modular software.

In contrast, the

Coq

proof development environment provides a powerful program logic (CiC) coupled with an extensible, interactive environment that can combine deep insights from humans with automation to discharge deep proof obligations. Unfortunately, the language at the core of

Coq

is limited to purely functional programming.

In the

Ynot

project, we are attempting to address this problem by extending

Coq

with a new type constructor (the Hoare-triple type), and a few carefully chosen axioms that can be used to build imperative programs in a style quite close to

Haskell

. I will report on our progress thus far, both in using

Ynot

to construct modular, extensible libraries for imperative programs, as well as our new compiler infrastructure for generating efficient code from

Ynot

programs.