888888 88 88 88 88 88 888 8888 8888 88 88 8888 88 88 88 88 88 88 88 88 88 88 88 888 88 88 8888 88 888 88 88 88 88 88 88 88 8888 8888 88 88 8888 888888 88 88888 88 88 88888
Jitawa — a verified Lisp runtime for MilawaThis page contains source code, documentation and proofs scripts relating to a verified Lisp runtime, called Jitawa. Jitawa was designed to host Jared Davis' Milawa theorem prover — a prover which we have formally proved to be sound when run on Jitawa.
The HOL4-verification of Jitawa is described in the following paper.Magnus O. Myreen and Jared Davis.
A verified runtime for a verified theorem prover.
In Interactive Theorem Proving (ITP), 2011.
Our soundness proof for the Milawa theorem prover is described in:Magnus O. Myreen and Jared Davis.And a supporting technique which aids program verification and code synthesis is described in:
The reflective Milawa theorem prover is sound (down to the machine code that runs it).
Draft.Magnus O. Myreen.
Functional programs: conversions between deep and shallow embeddings.
To appear in Interactive Theorem Proving (ITP), 2012.
The above papers are based on proofs scripts which are available under the HOL/examples/theorem-prover folder in the github repository for the HOL4 theorem prover. In particular, this folder contains the definition of the operational semantics which Jitawa has been proved to implement. We have formalised s-expression and parsing of s-expression. This github folder also contains our formalisation of Milawa's logic and the source code for the Milawa kernel which we have proved sound. Details are also available regarding the x86 implementation of Jitawa, e.g. the copying garbage collector which we have verified can be seen in these proof scripts.
Code and documentation
Download the latest version of Jitawa's sources here. To compile Jitawa, just run make in the directory of its sources. The executable is called jitawa. You will need gcc on a 64-bit x86 machine running Linux or Mac OS X.
A short introduction to using Jitawa can be found here.
Sources and documentation regarding the Milawa theorem prover can be found on Jared Davis' website.