Name
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. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-17164-2_30 | APLAS |
Keywords | Field | DocType |
first-class lock,logical mix,minor project,contravariant circularity,mechanized semantic library,semantic definition,resource accounting,concurrent c | Intuitionistic logic,Separation logic,Programming language,Computer science,Program logic,Theoretical computer science,Covariance and contravariance of vectors,Invariant (mathematics),Modular design,Kripke models | Conference |
Volume | ISSN | ISBN |
6461 | 0302-9743 | 3-642-17163-X |
Citations | PageRank | References |
2 | 0.41 | 12 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Aquinas Hobor | 1 | 243 | 17.42 |
| Robert Dockins | 2 | 75 | 3.93 |
| Andrew W. Appel | 3 | 2599 | 292.71 |