This repository contains my report and Agda implementation for my Master's Thesis titled:
Mechanizing Hoare Style Proof Outlines for Imperative Programs in Agda
The library defines Hoare triples and a syntax for writing outlines independent of target language or store implementation. The mechanization aims to make the outlines more readable by using macros in Agda to solve tedious proofs.
The thesis can be found at the TU Delft repository.
The main source is in src/.
See Everything.agda for a complete overview and description of all modules in the library.
Examples of how to use the library are contained in examples/.
The library depends on:
The correct versions of these dependencies are included in lib/ as git submodules, so make sure you recursively clone the repository.
See the Agda documentation on how to install Agda and libraries for your system.
You can check the entire library by running the following in the root of the repository:
$ agda -i. Everything.agda
It might take a minute or two for the type checking to finish.
The library is checked using --safe and --without-K.