[isabelle] NEW AFP entry: Shivers' Control Flow Analysis

by Joachim Breitner

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 using the logic HOLCF in theorem prover Isabelle.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.