Refinement with Time - Refining the Run-time of Algorithms in Isabelle/HOL

Browse Theories online

Good entry points are the following theories:

Sepreftime
This theory defines NREST and develops the lst calculus.
Sepref_Basic
This theory establishes the connection between NREST and Imperative/HOL with time by defining hn_refine and proving synthesis rules.
Examples
This theory collects the examples Remdups, Binary Search, Floyd Warshall, Kruskal and Edmonds-Karp. It can be used to further explore these examples.

All theories can be browsed here. Also see the theory dependency graph.

Use Theories

Get:

Download archive here.

Setup:

  1. Get Isabelle2018 (https://isabelle.in.tum.de/)
  2. Extract the zip file to /path/to/folder
  3. add `/path/to/folder` to ~/.isabelle/Isabelle2018/ROOTS
    NOTE: this submission comes with an specific version of the AFP. If the AFP is registered in the $ISABELLE_USER_HOME/ROOTS please uncomment it in order to use this version.

Check theories:

  1. navigate to /path/to/folder/Sepreftime/Sepreftime
  2. /path/to/Isabelle2018/bin/isabelle build -D .
    Building the theories may take a while. But beware to not build from the root folder of the archive (where the README resides) but from within the /Sepreftime subfolder!

Browse theories:

  1. navigate to /path/to/folder/Sepreftime/Sepreftime
  2. /path/to/Isabelle2018/bin/isabelle jedit -l SeprefTime_Base Examples/Examples.thy