Joachim Breitner's Homepage

As my student research project I worked on a formalization of Olin Shiver’s control flow algorithms for functional languages (as written down in his dissertation) in the theorem prover Isabelle. I just handed in my report to my supervisor Andreas Lochbihler. I have also submitted the Isabelle theories to the archive of formal proofs and uploaded the Haskell prototype on Hackage. The complete code is in a git repository.