The Mechanized Semantic Library is a collection of mathematical techniques useful for developing semantic models of program logics and type systems: separation algebras, permission share models, indirection theory (a clean axiomatization of step indexing), and modal logics.

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.

Software distribution

The current version of MSL is distributed as a component of the Verified Software Toolchain. The MSL component will build by itself.

Release versions.
Bleeding-edge in the Subversion repository.

History

Older versions: 0.1, 0.2, 0.3.

MSL v0.3 has the following enhancements over v0.2:

MSL v0.2 has the following enhancements over v0.1:

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]
3. Shares Share accounting to model fractional ownership in separation logic [2]
4. Indirection Theory Semantic models for approximating contravariant circularities [3], [4]
5. Logics Definitions of substructural and modal logics [1], [2], [3], [4]

Publications

# Title Authors Read Cite
[1] Multimodal Separation Logic
for Reasoning About Operational Semantics
R. Dockins, A. W. Appel, A. Hobor PDF BibTeX
[2] A Fresh Look at Separation Algebras and Share Accounting R. Dockins, A. Hobor, A. W. Appel PDF BibTeX
[3] A Theory of Indirection via Approximation A. Hobor, R. Dockins, A. W. Appel PDF BibTeX
[4] A Logical Mix of Approximation and Separation A. Hobor, R. Dockins, A. W. Appel PDF BibTeX

List order is by publication date.  For a mapping of files to papers please see the file list.

Presentations

# Title Authors Read Cite
[1] Developing and Mechanizing Semantic Models
for Program Logics
A. Hobor, R. Dockins PDF -

Examples

The MSL includes some associated examples using various components of the library.  The first example, released with v0.2, is a mechanized type soundness proof for the polymorphic lambda calculus with references.  The second example, released with v0.3, is a separation logic for a simple imperative language with loops and functions.  We plan to include more examples as we continue to build the MSL.  These examples are released under the same BSD-style license as the MSL.

# Example Components
1 Type Soundness of the Polymorphic Lambda Calculus with References Indirection Theory, Logics
2 Separation Logic for While Programs with Functions Separation Algebras, Logics

Projects using the Mechanized Semantic Library

The following projects use the MSL.  Although the MSL is utilized in them, and in some cases was developed in conjunction with them, they are independent projects, with their own developers, goals, codebase, and associated license schemes.

Verified Software Toolchain

The goal of the Verified Software Toolchain Project is to connect machine-verified source programs to machine-verified optimizing compilers.  This project grew out of the Concurrent C Minor project, which involved the design and soundness proof of a concurrent separation logic with first-class locks and threads for a variant of Xavier Leroy's C minor language.

Barriers in Concurrent Separation Logic

Design and soundness proof for a concurrent separation logic for Pthreads-style barriers.

Heap-Hop

Heap-Hop is a prover for concurrent heap-manipulating programs that use Hoare monitors and message-passing synchronization. Programs are annotated with pre and post-conditions and loop invariants, written in a fragment of separation logic. Communications are governed by a form of session types called contracts. Heap-Hop can prove safety and race-freedom and, thanks to contracts, absence of memory leaks and safety of communications. [Text from Heap-Hop website]

File list

# File name Line count     Component Associated paper(s)
1. Axioms.v 48   Base
2. Extensionality.v 96   Base  
3. base.v 119   Base  
4. sepalg.v 681   Separation Algebras [2]
5. cjoins.v 148   Separation Algebras  
6. sepalg_generators.v 960   Separation Algebras [2], [3], [4]
7. cross_split.v 494   Separation Algebras [2]
8. join_hom_lemmas.v 421   Separation Algebras [3], [4]
9. boolean_alg.v 433   Shares [2]
10. tree_shares.v 2,427   Shares [2]
11. shares.v 1,119   Shares [2]
12. extract.v 13   Shares  
13. knot.v 489   Indirection Theory [3]
14. knot_hered.v 675   Indirection Theory [4]
15. knot_full.v 1,023   Indirection Theory  
16. knot_lemmas.v 118   Indirection Theory [3]
17. knot_sa.v 429   Indirection Theory [3], [4]
18. knot_sa_trivial.v 51   Indirection Theory  
19. knot_shims.v 1,599   Indirection Theory  
20. knot_prop.v 349   Indirection Theory  
21. sepalg_functors.v 409   Indirection Theory [4]
22. knot_setoid.v 601   Indirection Theory [3]
23. knot_unique.v 1,000   Indirection Theory [3]
24. ageable.v 524   Logics [4]
25. age_sepalg.v 328   Logics [3], [4]
26. predicates_hered.v 811   Logics [1], [2], [3], [4]
27. predicates_sl.v 392   Logics [1], [2], [3], [4]
28. subtypes.v 186   Logics [1], [4]
29. predicates_rec.v 322   Logics [1], [4]
30. contractive.v 502   Logics [1], [4]
31. msl_standard.v 21   MSL  
           
  Total 16,788   MSL [1], [2], [3], [4]

Component Details

Base

Axioms.v
This file contains the axiom base for the development. We assume dependent functional extensionality and propositional extensionality. These axioms are compatible with the law of excluded middle, dependent unique choice, relational choice, etc.

Extensionality.v
Consequences of the extensionality axioms.

base.v
This exports the parts of the Coq standard library used throughout the development, our axioms and extensionality facts, and a few custom convenience tactics.

Separation Algebras

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.

cjoins.v
This file defines a constructive version of some of the (existential) join definitions, such as join_sub and joins.

sepalg_generators.v
We define SA operators in this file. All the operators mentioned in [2] (except for the boolean algebra generator, located in the shares component), [3], and [4] appear here, along with a few others.

cross_split.v
We define and prove properties about the cross_split axoim discussed in [2], including the relationship to distributive separation algebras and how to pull the property through many of the generators.

join_hom_lemmas.v
A series of lemmas that can be used to prove that functions are join homomorphisms as defined in [3] and [4], although the lemmas themselves are not covered in any paper.

Shares

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.

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.

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.

extract.v
This file will compile the share model into OCaml code for program analysis tools.  Read the instructions to see how.

Indirection Theory

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.

knot_hered.v
Enhances knot.v by threading a monotonicity property through the construction.  The result is that all predicates extracted from a knot are automatically hereditary.  Although the axiomatization is not much more complex than in the basic case, the construction is significantly harder.  The axiomatization is explained in section 2.3 of [4]; the construction will be explained in a future paper.
knot_full.v
Enhances knot_hered.v to allow the input to the knot to be a bifunctor, and allow the user to supply a relation that further restricts the predicates that can be stored in the knot.  The axiomatization is slightly more complicated than in the knot_hered case, but the construction is again more complicated.  This file will be explained in a future paper.
knot_lemmas.v
Easy lemmas that follow from the theory of indirection, including a Galois connection.

knot_sa.v
The definition of a separation algebra on top of knots as coved in section 7 of [3] and in more detail in sections 6 and 7 of [4].

knot_sa_trivial.v
Used when you want to use the logics module, but do not have interesting separation behavior.

knot_shims.v
Defines knot interfaces for common cases (e.g., when we do not need the bifunctor) and provides shims that translate to knot_full.

knot_prop.v
This file specializes the knot, knot_lemmas, and knot_sa files to use "Prop" as truth values.

sepalg_functors.v
A technical development of "unmapping" needed to get the extra unage* properties in knot_sa as explained in section 7 of [4].

knot_setoid.v
An alternate, axiom-free, development of the knot. We avoid the need for the extensionality axiom by working explicitly up to equivalence relations and weakening the axioms of the theory accordingly.  Not mainline due to lack of use and long build time.

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

ageable.v
Define a
notion of approximation as in section 2 of [4] as the "ageable" typeclass.

age_sepalg.v
We enhance separation algebras with as in section 6 of [4]. The "ASA" typeclass presents an interface sufficient to define the Kripke model below. The interface is implemented using the properties obtained from knot_sa.

predicates_hered.v
Definition of higher-order modal logic as discussed in sections 2, 4, and 5 of [1]; briefly in section 4 of [2]; sections 5 and 6 of [3]; and sections 2 and 3 of [4].

predicates_sl.v
Definition of higher-order separation logic as discussed in section 6 of [1], section 4 of [2], section 7 of [3], and section 6 of [4].

subtypes.v
Lemmas about fashionable implication. This is partially explained in section 4 of [4].

predicates_rec.v
Definition and proofs about equirecursion.  We include both the standard "mu" recursion as well as a more powerful higher-order variant.  This file is partially explained in section 5 of [1] and section 4 of [4] and will be explained in more detail in a future paper.

contractive.v
A collection of utility lemmas for proving that various predicate functions are contractive or nonexpansive (for both the regular recursion and the higher-order variety).  This file is partially explained in section 4 of [4] and will be explained in more detail in a future paper.

MSL

msl_standard.v
A file which re-exports the major components of the MSL library for users.

People

The Mechanized Semantic Library was developed by Andrew W. Appel, Robert Dockins, and Aquinas Hobor.

License

Copyright (c) 2009-2010, 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.