CeTA's Framework for Developing Stand-Alone Certifiers
This website accompanies the paper CeTA's Framework for Developing Stand-Alone Certifiers and provides all relevant Isabelle theory files and examples.
A bundle of all relevant files is available here. Unpacking it will result in the following files and directories:
Makefile |
a Makefile for code generation and compilation of the resulting Haskell program | |
ROOTS |
an Isabelle config file telling the system where to look for sessions | |
thys |
a directory containing all necessary theory files | |
src |
a directory containing the sources of the main Haskell function that puts all the generated code together to obtain an executable certifier | |
examples |
a directory containing some example inputs for the resulting certifier
pcp |
In order to obtain the certifier (pcp) do the following on a
command line (which requires Isabelle2015, the corresponding archive of
formal proofs, as well as the GHC Haskell compiler in order to succeed):
$ make
Note: See here for the LSFA 2014 paper A Framework for Developing Stand-Alone Certifiers.