We have verified several versions of the CPS transformation in Isabelle/HOL. In our verification we adopted first-order abstract syntax with variable names so that the formalization is close to that of hand-written proofs and compilers. To simplify treatment of fresh variables introduced by the transformation, we introduced abstract syntax parameterized with the type of variables. We also found that the standard formalization of alpha-equivalence was cumbersome for theorem provers and reformulated alpha-equivalence as a syntax-directed deductive system. To simplify verification of the CPS transformation for the language extended let-expressions, it was essential to impose that variables are uniquely used in a program.
To obtain a correct compiler, it is not enough to show its formalization is correct, but it is also required to show that the implementation of the compiler is correct. We formalized a compiler with the theorem prover Isabelle/HOL, and proved its correctness. Then, we translated the compiler definition from Isabelle/HOL into a Standrad ML program, using Isabelle/HOL's code generation facility. Since this code generation program only performs simple syntactic translation, the correctness of the obtained program can be highly trusted. The compiler we defined with Isabelle/HOL covers all phases of the compiler, except a front-end. We provided a hand-written parsing program, and obtained a verified, executable compiler. Our compiler compiles a functional language similar to Scheme into a Java virtual machine assembly language. It includes several non-trivial program transformations such as closure conversion and inline expansion. Taking compilation time into consideration, we chose efficient data structures in our specification. Benchmarks show that our compiler is comparable to existing compilers both in compilation time and running time.
Depth-first search of a graph is formalized with recdef. It is shown that it visits all of the reachable nodes from a given list of nodes. Executable ML code of depth-first search is obtained using the code generation feature of Isabelle/HOL.
I have contributed the output module for Isabelle/HOL for the verification tool Why and Caduceus. I have verified with Caducues and Isabell/HOL several C programs including the bubble sort and the Tortoise Hare algorithm that checks if a list contains a cycle or not.