Library index
The development is made of
- notations
- Kleene fixpoint theorems
- Results about finite types
- Core Object-Oriented Language definition
- Context-sensitive instrumented semantics with equivalence proofs
- The parametrised Points-to analysis with soundness proofs
- The proof that CPA beats oo-CFA The source code is available here
This page has been generated by coqdoc