A logical mix of approximation and separation

Abstract

We extract techniques developed in the Concurrent C minor project to build a framework for constructing logics that contain approximation and/or separation. Approximation occurs when the naïve semantic definitions contain a contravariant circularity (e.g., invariants of first-class locks), while separation occurs when one wishes to track resource accounting. We show how these two features can be mixed together in a modular way. Our work is machine checked in Coq and available as part of the Mechanized Semantic Library. © 2010 Springer-Verlag.