TY - GEN
T1 - A logical mix of approximation and separation
AU - Hobor, Aquinas
AU - Dockins, Robert
AU - Appel, Andrew W.
N1 - Funding Information:
Acknowledgements. Aquinas Hobor is supported by a Lee Kuan Yew Postdoctoral Fellowship. Robert Dockins and Andrew W. Appel are supported in part by NSF grant CNS-0910448 and AFOSR grant FA9550-09-1-0138.
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=78650732614&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=78650732614&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-17164-2_30
DO - 10.1007/978-3-642-17164-2_30
M3 - Conference contribution
AN - SCOPUS:78650732614
SN - 364217163X
SN - 9783642171635
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 439
EP - 454
BT - Programming Languages and Systems - 8th Asian Symposium, APLAS 2010, Proceedings
T2 - 8th Asian Symposium on Programming Languages and Systems, APLAS 2010
Y2 - 28 November 2010 through 1 December 2010
ER -