Joachim Breitner

Student research project on Shivers’ control flow algorithm

Published 2010-11-16 in sections English, Digital World.

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.


Have something to say? You can post a comment by sending an e-Mail to me at <>, and I will include it here.