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

Miscellaneous

Finite maps

Operational semantics

Axiomatic semantics