A Verified Compiler in Isabelle/HOL

We are trying to build an another verified compiler based on our APLAS paper. In this page, you can find proof scripts and document(proofs) produced by Isabelle/HOL.

Currently, we are cleaning up our proofs.

Proof Scripts and Documents(APLAS)

Proof scripts works with Isabelle 2003. Our proof scripts uses X-symbol package intensivly. If you are not using it, please consult the document produced by Isabelle.

• Proof scripts for compiler specification: vc.tar.gz
• Proof documents produced by Isabelle: vc-aplas.ps

Proof Scripts and Documents(ISPJ PRO)

Here is our latest proof script of our compiler(04/09/28). Proof scripts work with Isabelle 2004.

• Proof scripts for compiler specification: vc-20040928.tar.gz
• Proof documents produced by Isabelle: vc-pro.ps

Back to my homepage