Hoare Type Theory

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

Building and executing artifacts

Requirements

Coq 8.5pl3 (available from https://coq.inria.fr/coq-85)
Mathematical Components 1.6.1 (http://math-comp.github.io/math-comp/)

After installing SSReflect, make sure to have the following environment variables properly declared.

Build

make clean; make