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 Milawa

This 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.

Papers

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.
The reflective Milawa theorem prover is sound (down to the machine code that runs it).
Submitted to Interactive Theorem Proving (ITP), 2014.

And a supporting technique which aids program verification and code synthesis is described in:

Magnus O. Myreen.
Functional programs: conversions between deep and shallow embeddings.
In Interactive Theorem Proving (ITP), 2012.

Proof scripts

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.