The CH₂O 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

• memory: the memory model.
• expressions: expressions and their semantics.
• statements: statements and program contexts.
• state: the execution state.
• smallstep: the small step operational semantics.

Axiomatic semantics

• assertions:assertions of the axiomatic semantics.
• axiomatic: axiomatic semantics using separation logic.
• gcd: verification of Euclid's algorithm.