@inproceedings{jung_iris:_2015,
	address = {New York, NY, USA},
	series = {{POPL} '15},
	title = {Iris: {Monoids} and {Invariants} as an {Orthogonal} {Basis} for {Concurrent} {Reasoning}},
	volume = {50},
	isbn = {978-1-4503-3300-9},
	shorttitle = {Iris},
	url = {http://doi.acm.org/10.1145/2676726.2676980},
	doi = {10/gf8t7m},
	abstract = {We present Iris, a concurrent separation logic with a simple premise: monoids and invariants are all you need. Partial commutative monoids enable us to express---and invariants enable us to enforce---user-defined *protocols* on shared state, which are at the conceptual core of most recent program logics for concurrency. Furthermore, through a novel extension of the concept of a *view shift*, Iris supports the encoding of *logically atomic specifications*, i.e., Hoare-style specs that permit the client of an operation to treat the operation essentially as if it were atomic, even if it is not.},
	urldate = {2019-09-24},
	booktitle = {Proceedings of the {42Nd} {Annual} {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages}},
	publisher = {ACM},
	author = {Jung, Ralf and Swasey, David and Sieczkowski, Filip and Svendsen, Kasper and Turon, Aaron and Birkedal, Lars and Dreyer, Derek},
	month = jan,
	year = {2015},
	note = {event-place: Mumbai, India
Citation Key Alias: jung2015},
	pages = {637--650}
}

{"_id":"Lpt77Mbg8c6GAWY2G","bibbaseid":"jung-swasey-sieczkowski-svendsen-turon-birkedal-dreyer-irismonoidsandinvariantsasanorthogonalbasisforconcurrentreasoning-2015","authorIDs":[],"author_short":["Jung, R.","Swasey, D.","Sieczkowski, F.","Svendsen, K.","Turon, A.","Birkedal, L.","Dreyer, D."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","address":"New York, NY, USA","series":"POPL '15","title":"Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning","volume":"50","isbn":"978-1-4503-3300-9","shorttitle":"Iris","url":"http://doi.acm.org/10.1145/2676726.2676980","doi":"10/gf8t7m","abstract":"We present Iris, a concurrent separation logic with a simple premise: monoids and invariants are all you need. Partial commutative monoids enable us to express—and invariants enable us to enforce—user-defined *protocols* on shared state, which are at the conceptual core of most recent program logics for concurrency. Furthermore, through a novel extension of the concept of a *view shift*, Iris supports the encoding of *logically atomic specifications*, i.e., Hoare-style specs that permit the client of an operation to treat the operation essentially as if it were atomic, even if it is not.","urldate":"2019-09-24","booktitle":"Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","publisher":"ACM","author":[{"propositions":[],"lastnames":["Jung"],"firstnames":["Ralf"],"suffixes":[]},{"propositions":[],"lastnames":["Swasey"],"firstnames":["David"],"suffixes":[]},{"propositions":[],"lastnames":["Sieczkowski"],"firstnames":["Filip"],"suffixes":[]},{"propositions":[],"lastnames":["Svendsen"],"firstnames":["Kasper"],"suffixes":[]},{"propositions":[],"lastnames":["Turon"],"firstnames":["Aaron"],"suffixes":[]},{"propositions":[],"lastnames":["Birkedal"],"firstnames":["Lars"],"suffixes":[]},{"propositions":[],"lastnames":["Dreyer"],"firstnames":["Derek"],"suffixes":[]}],"month":"January","year":"2015","note":"event-place: Mumbai, India Citation Key Alias: jung2015","pages":"637–650","bibtex":"@inproceedings{jung_iris:_2015,\n\taddress = {New York, NY, USA},\n\tseries = {{POPL} '15},\n\ttitle = {Iris: {Monoids} and {Invariants} as an {Orthogonal} {Basis} for {Concurrent} {Reasoning}},\n\tvolume = {50},\n\tisbn = {978-1-4503-3300-9},\n\tshorttitle = {Iris},\n\turl = {http://doi.acm.org/10.1145/2676726.2676980},\n\tdoi = {10/gf8t7m},\n\tabstract = {We present Iris, a concurrent separation logic with a simple premise: monoids and invariants are all you need. Partial commutative monoids enable us to express---and invariants enable us to enforce---user-defined *protocols* on shared state, which are at the conceptual core of most recent program logics for concurrency. Furthermore, through a novel extension of the concept of a *view shift*, Iris supports the encoding of *logically atomic specifications*, i.e., Hoare-style specs that permit the client of an operation to treat the operation essentially as if it were atomic, even if it is not.},\n\turldate = {2019-09-24},\n\tbooktitle = {Proceedings of the {42Nd} {Annual} {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages}},\n\tpublisher = {ACM},\n\tauthor = {Jung, Ralf and Swasey, David and Sieczkowski, Filip and Svendsen, Kasper and Turon, Aaron and Birkedal, Lars and Dreyer, Derek},\n\tmonth = jan,\n\tyear = {2015},\n\tnote = {event-place: Mumbai, India\nCitation Key Alias: jung2015},\n\tpages = {637--650}\n}\n\n","author_short":["Jung, R.","Swasey, D.","Sieczkowski, F.","Svendsen, K.","Turon, A.","Birkedal, L.","Dreyer, D."],"key":"jung_iris:_2015","id":"jung_iris:_2015","bibbaseid":"jung-swasey-sieczkowski-svendsen-turon-birkedal-dreyer-irismonoidsandinvariantsasanorthogonalbasisforconcurrentreasoning-2015","role":"author","urls":{"Paper":"http://doi.acm.org/10.1145/2676726.2676980"},"downloads":0},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/k4rtik","creationDate":"2019-07-02T12:17:56.627Z","downloads":0,"keywords":[],"search_terms":["iris","monoids","invariants","orthogonal","basis","concurrent","reasoning","jung","swasey","sieczkowski","svendsen","turon","birkedal","dreyer"],"title":"Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning","year":2015,"dataSources":["Z5Dp3qAJiMzxtvKMq"]}