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
Topics
Session Shivers-CFA
- HOLCFUtils
- CPSScheme
- Eval
- Utils
- SetMap
- AbsCF
- ExCF
- AbsCFCorrect
- ExCFSV
- Computability
- FixTransform
- CPSUtils
- MapSets
- AbsCFComp