CiteULike is a free online bibliography manager. Register and you can start organising your references online.
Tags

Concurrent Separation Logic and Operational Semantics

by: Viktor Vafeiadis
Electron. Notes Theor. Comput. Sci., Vol. 276 (September 2011), pp. 335-351, doi:10.1016/j.entcs.2011.09.029  Key: citeulike:9947768

Formatted Citation


Show HTML

Likes (beta)

This copy of the article hasn't been liked by anyone yet.

View FullText article


Abstract

This paper presents a new soundness proof for concurrent separation logic (CSL) in terms of a standard operational semantics. The proof gives a direct meaning to CSL judgments, which can easily be adapted to accommodate extensions of CSL, such as permissions and storable locks, as well as more advanced program logics, such as RGSep. Further, it explains clearly why resource invariants should be 'precise' in proofs using the conjunction rule.


kozima's tags for this article

Citations (CiTO)

No CiTO relationships defined

X There are no reviews yet

X Posting History


X Export records

Privacy Statement | Terms & Conditions
CiteULike organises scholarly (or academic) papers or literature and provides bibliographic (which means it makes bibliographies) for universities and higher education establishments. It helps undergraduates and postgraduates. People studying for PhDs or in postdoctoral (postdoc) positions. The service is similar in scope to EndNote or RefWorks or any other reference manager like BibTeX, but it is a social bookmarking service for scientists and humanities researchers.