Separation Logic Implementation in Coq


Technical documents

See here for further information.

Bigtoe: A Certified Verifier for a Fragment of Separation Logic

Coq Implementation Overview

The whole archive: seplog.tgz, CVS browser (As of August 2007, a more recent version is available here)

Contact information: reynald dot affeldt at aist dot go dot jp