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 <mail@joachim-breitner.de>, and I will include it here.
Photos