Version: 0.1
About
The Mechanized Semantic Library is a collection of mathematical techniques useful for developing semantic models of program logics and type systems. The library has a special emphasis on techniques which integrate smoothly into a mechanical theorem prover; at the moment the library is only available for use in Coq.
Download entire MSL, version 0.1
Note: v0.1 is no longer the most recent version.
The Mechanized Semantic Library is made available under a BSD-style license.
Component Overview
| # | Name | Description | Paper(s) |
| 1. | Base | Axioms for computation; custom tactics; basic theorems | |
| 2. | Separation Algebras | Compositional semantic models for separation logic | [2], [3] |
| 4. | Shares | Share accounting to model fractional ownership in separation logic | [2] |
| 5. | Indirection Theory | Semantic models for approximating contravariant circularities | [3] |
| 6. | Logics | Definitions of substructural and modal logics | [1], [2], [3] |
Publications
| # | Title | Authors | Read | Cite |
| [1] | Multimodal Separation Logic for Reasoning About Operational Semantics |
R. Dockins, A. W. Appel, A. Hobor | BibTeX | |
| [2] | A Fresh Look at Separation Algebras and Share Accounting | R. Dockins, A. Hobor, A. W. Appel | BibTeX | |
| [3] | A Theory of Indirection via Approximation | A. Hobor, R. Dockins, A. W. Appel | BibTeX |
List order is by publication date. For a mapping of files to papers please see the file list.
Projects using the Mechanized Semantic Library
Concurrent C Minor
The goal of the Concurrent C Minor Project is to connect machine-verified source programs in sequential and concurrent programming languages to machine-verified optimizing compilers.
File list
| # | File name | Component | Associated paper(s) |
| 1. | ClassicalReasoningAboutComputation.v | Base | |
| 2. | base.v | Base | |
| 3. | sepalg.v | Separation Algebras | [2] |
| 4. | sepalg_generators.v | Separation Algebras | [2], [3] |
| 5. | boolean_alg.v | Shares | [2] |
| 6. | tree_shares.v | Shares | [2] |
| 7. | shares.v | Shares | [2] |
| 8. | knot.v | Indirection Theory | [3] |
| 9. | knot_setoid.v | Indirection Theory | [3] |
| 10. | knot_lemmas.v | Indirection Theory | [3] |
| 11. | knot_sa.v | Indirection Theory | [3] |
| 12. | knot_prop.v | Indirection Theory | |
| 13. | sepalg_functors.v | Indirection Theory | |
| 14. | knot_unique.v | Indirection Theory | [3] |
| 15. | age_sepalg.v | Logics | [3] |
| 16. | predicates_hered.v | Logics | [1], [2], [3] |
Component Details
Base
Download
ClassicalReasoningAboutComputation.v
This file contains the axiom base for the development. We assume the classical
axiom, dependent unique choice, relational choice, functional extensionality and
propositional extensionality. However, the proofs in this distribution use only
the extensionality axioms.
Download base.v
This exports the parts of the Coq standard library used throughout the
development as well as a few custom convenience tactics.
Separation Algebras
Download sepalg.v
This file defines our relational form of separation algebras with the
disjointness axiom. We also define the join_sub relation and the joins relation.
Additionally, elementary lemmas about the definitions are proved.
Download
sepalg_generators.v
We define SA operators in this file. All the operators mentioned in
[2] and [3] appear here, along with
a few others.
Shares
Download
boolean_alg.v
This file defines boolean algebras from an order-theoretic perspective. We also
define axioms relating to properties we desire of share models, including
relativization, splitting and token factory axioms.
Download
tree_shares.v
Here we construct the boolean-labeled tree share model as discussed in
[2]. Note, however, that the proof of the token counting
axioms follow a slightly different path than the proof in that paper. This
is mostly because reasoning about sets in Coq is inconvenient.
Download shares.v
This file simply repackages the construction from tree_shares.v into a nicer
interface for downstream users. We also define the notion of a "positive" share;
that is a nonunit share.
Indirection Theory
Download
knot.v
This file contains the central "knot" development used to model approximations
to contravariant circularities. Included are both the axiomitization and the
model construction. It follows section 8 of [3] quite
closely.
Download
knot_setoid.v
An alternate, axiom-free, development of the knot. We avoid the need for the
extensionality axiom by working explicitly up to equivalance relations and
weakening the axioms of the theory accordingly.
Download
knot_lemmas.v
Easy lemmas that follow from the theory of indirection.
Download
knot_sa.v
The definition of a separation algebra on top of knots. In addition to the
properties mentioned in [3], this development adds several
properties (unage_join1 and unage_join2), which require the additional input
axiom F_preserves_unmaps. These properties will be covered in an upcoming
paper.
Download
knot_prop.v
This file specializes the knot and knot_sa constructions to use "Prop" as truth
values.
Download
sepalg_functors.v
A technical development of "unmapping" needed to get the extra unage*
properties in knot_sa.
Download
knot_unique.v
The development of the uniqueness proof for knots. We prove that any two
implementations of the theory of indirection are isomorphic.
Logics
Download
age_sepalg.v
We enhance the signature of separation algebras with a notion of aging. The
"ASA" typeclass presents an interface sufficient to define the Kripke model
below. The interface is straightforwardly implemented using the properties
obtained from knot_sa.
Download
predicates_hered.v
Definition of the higher-order modal separation logic as discussed in sections
2, 4, 5, and 6 of [1]; section 4
of [2]; and sections 5, 6, and 7 of [3].
People
The Mechanized Semantic Library is developed and maintained by Andrew W. Appel, Robert Dockins, and Aquinas Hobor.
License
Copyright (c) 2009, Andrew Appel, Robert Dockins and Aquinas Hobor.
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
- Redistribution of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
- Redistribution in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR THE CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.