The CH2O formalization
By Robbert Krebbers, Radboud University Nijmegen
About
This is the Coq formalization corresponding to the FoSSaCS 2013 paper Separation Logic for Non-local Control Flow and Block Scope Variables by Robbert Krebbers and Freek Wiedijk.
The continued development can be found here.
Download
The source code of this development can be downloaded here.
Table of contents
Prelude
- base: interfaces, notations, and general theorems.
- tactics: general purpose tactics.
- decidable: theorems on decidable structures.
- orders: theorems on ordered structures.
- option: miscellaneous definitions and theorems on the option data type.
- list: miscellaneous definitions and theorems on lists.
- vector: miscellaneous definitions and theorems on vectors.
- numbers: miscellaneous facts on nat, N and Z.
- ars: theorems and definitions on abstract rewriting systems.
- collections: definitions, theorems, and tactics for collections.
- fin_collections: theorems on finite collections.
- listset: finite set implementation using unordered lists.
- numbers: generation of fresh numbers.
- prelude: exports all of the above.
Miscellaneous
- listset_nodup: finite set implementation using unordered lists without duplicates.
Finite maps
- fin_maps: an interface and theorems for finite maps.
- pmap: finite map indexed by positive.
- nmap: finite map indexed by N.
Operational semantics
Axiomatic semantics
- assertions:assertions of the axiomatic semantics.
- axiomatic: axiomatic semantics using separation logic.
- gcd: verification of Euclid's algorithm.