Shivers' Control Flow Analysis

Title:	Shivers' Control Flow Analysis
Author:	Joachim Breitner (mail /at/ joachim-breitner /dot/ de)
Submission date:	2010-11-16
Abstract:	In his dissertation, Olin Shivers introduces a concept of control flow graphs for functional languages, provides an algorithm to statically derive a safe approximation of the control flow graph and proves this algorithm correct. In this research project, Shivers' algorithms and proofs are formalized in the HOLCF extension of HOL.
License:	BSD License

Proof outline Proof document

Browse theories

Download this entry

Older releases: Isabelle 2011: afp-Shivers-CFA-2011-02-11.tar.gz Isabelle 2009-2: afp-Shivers-CFA-2010-11-18.tar.gz Isabelle 2009-2: afp-Shivers-CFA-2010-11-17.tar.gz