The Coq mailing list

[Alexander Gryzlov <alex.gryzlov AT gmail.com>]

Hello,

We would like to announce the first public release of Hoare Type Theory (HTT), a verification system for reasoning about sequential heap-manipulating programs based on Separation logic. It is available on Github (https://github.com/imdea-software/htt) and can be installed via opam.

HTT incorporates Hoare-style specifications via preconditions and postconditions into types. A Hoare type `ST P (fun x : A => Q)` denotes computations with a precondition `P` and postcondition `Q`, returning a value `x` of type `A`. Hoare types are a dependently typed version of monads, as used in the programming language Haskell. Monads hygienically combine the language features for pure functional programming, with those for imperative programming, such as state or exceptions. In this sense, HTT establishes a formal connection in the style of Curry-Howard isomorphism between monads and (functional programming variant of) Separation logic. Every effectful command in HTT has a type that corresponds to the appropriate non-structural inference rule in Separation logic, and vice versa, every non-structural inference rule corresponds to a command in HTT that has that rule as the type. The type for monadic bind is the Hoare rule for sequential composition, and the type for monadic unit combines the Hoare rules for the idle program (in a small-footprint variant) and for variable assignment (adapted for functional variables). The connection reconciles dependent types with effects of state and exceptions and establishes Separation logic as a type theory for such effects. In implementation terms, it means that HTT implements Separation logic as a shallow embedding in Coq.

The system is based on several papers: the original idea was introduced in "Polymorphism and Separation in Hoare Type Theory" (https://software.imdea.org/~aleks/papers/hoarelogic/icfp06.pdf) with "Dependent Type Theory of Stateful Higher-Order Functions" (https://software.imdea.org/~aleks/papers/hoarelogic/depstate.pdf) containing the initial motivation and preliminary proofs, while the version closest to the released implementation of HTT is described in "Structuring the Verification of Heap-Manipulating Programs" (http://software.imdea.org/~aleks/htt/reflect.pdf). You can find the full list of references on the Github page.

There are three main enhancements made in the current released version:

1. the Partial Commutative Monoid (PCM) structures used in the logic of assertions have been extracted into a separate https://github.com/imdea-software/fcsl-pcm project,
2. the Hoare types now use unary postconditions rather than VDM-style binary ones, and
3. the library has been refactored to support more powerful proof automation for heaps, based on canonical structures.

If you have any questions or suggestions for potential collaborations, please contact `aleks.nanevski [at] imdea.org`, or Alexander Gryzlov via zulip.

Best regards,
Aleks Nanevski & Alexander Gryzlov