A Framework for Developing Stand-Alone Certifiers
This website accompanies the paper A 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 |
sources of the main Haskell function that puts all the generated code together to obtain an executable certifier. | |
examples |
some example inputs for the resulting certifier
pcp |
In order to obtain the certifier (pcp) do the following on a
command line (which requires Isabelle2014, the corresponding archive of
formal proofs, as well as the GHC Haskell compiler in order to succeed):
$ make code $ make haskell
Then examples can be checked via:
$ ./pcp examples/p.pcp.xml