A logical mix of approximation and separation

Aquinas Hobor, Robert Dockins, Andrew W. Appel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 8th Asian Symposium, APLAS 2010, Proceedings
Pages439-454
Number of pages16
DOIs
StatePublished - Dec 1 2010
Event8th Asian Symposium on Programming Languages and Systems, APLAS 2010 - Shanghai, China
Duration: Nov 28 2010Dec 1 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6461 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other8th Asian Symposium on Programming Languages and Systems, APLAS 2010
CountryChina
CityShanghai
Period11/28/1012/1/10

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A logical mix of approximation and separation'. Together they form a unique fingerprint.

  • Cite this

    Hobor, A., Dockins, R., & Appel, A. W. (2010). A logical mix of approximation and separation. In Programming Languages and Systems - 8th Asian Symposium, APLAS 2010, Proceedings (pp. 439-454). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6461 LNCS). https://doi.org/10.1007/978-3-642-17164-2_30