Home

Awesome

Hoare Type Theory

This repository contains the main libraries of Hoare Type Theory (HTT) for reasoning about sequential heap-manipulating programs.

HTT is a verification system which incorporates Hoare style specifications via preconditions and postconditions, into types. A Hoare type {P}x : A{Q} denotes computations with a precondition P and postcondition Q, returning a value of type A. Hoare types are a dependently typed version of monads, as used in the programming language Haskell. Monads higenically 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 between Hoare logic and monads, in the style of Curry-Howard isomorphism: every effectful command in HTT has a type which corresponds to the appropriate inference rule in Hoare logic, and vice versa, every inference rule in (a version of) Hoare logic, corresponds to a command in HTT which has that rule as the type.

Building and executing artifacts

Requirements

For the installation, follow instructions in the corresponding README files.

Alternatively, Coq and mathcomp can be installed via the opam package manager, by executing the following commands in the console:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-ssreflect coq-fcsl-pcm

Build

make clean; make

Install

make install

Usage with opam

To install HTT as a opam package from your local repository, run the following command from the repository's root directory.

opam install .

References