@inproceedings{iris1,
author = {Jung, Ralf and Swasey, David and Sieczkowski, Filip and Svendsen, Kasper and Turon, Aaron and Birkedal, Lars and Dreyer, Derek},
title = {Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning},
year = {2015},
isbn = {9781450333009},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi-org.proxy.cc.uic.edu/10.1145/2676726.2676980},
doi = {10.1145/2676726.2676980},
booktitle = {Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
pages = {637–650},
numpages = {14},
keywords = {separation logic, higher-order logic, partial commutative monoids, compositional verification, fine-grained concurrency, atomicity, invariants},
location = {Mumbai, India},
series = {POPL ’15}
}

@inproceedings{hogs,
author = {Jung, Ralf and Krebbers, Robbert and Birkedal, Lars and Dreyer, Derek},
title = {Higher-Order Ghost State},
year = {2016},
isbn = {9781450342193},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi-org.proxy.cc.uic.edu/10.1145/2951913.2951943},
doi = {10.1145/2951913.2951943},
booktitle = {Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming},
pages = {256–269},
numpages = {14},
keywords = {higher- order logic, fine-grained concurrency, Separation logic, interactive theorem proving, compositional verification},
location = {Nara, Japan},
series = {ICFP 2016}
}

@article{iris-ground-up, title={Iris from the ground up: A modular foundation for higher-order concurrent separation logic}, volume={28}, DOI={10.1017/S0956796818000151}, journal={Journal of Functional Programming}, publisher={Cambridge University Press}, author={Jung, Ralf and Krebbers, Robbert and Jourdan, Jacques-Henri and Bizjak, Ale\v{s} and Birkedal, Lars and Dreyer, Derek}, year={2018}, pages={e20}}

@inproceedings{ipm,
author = {Krebbers, Robbert and Timany, Amin and Birkedal, Lars},
title = {Interactive Proofs in Higher-Order Concurrent Separation Logic},
year = {2017},
isbn = {9781450346603},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi-org.proxy.cc.uic.edu/10.1145/3009837.3009855},
doi = {10.1145/3009837.3009855},
booktitle = {Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages},
pages = {205–217},
numpages = {13},
keywords = {Coq, Fine-grained Concurrency, Interactive Theorem Proving, Logical Relations, Separation Logic},
location = {Paris, France},
series = {POPL 2017}
}

@InProceedings{igps,
  author =	{Jan-Oliver Kaiser and Hoang-Hai Dang and Derek Dreyer and Ori Lahav and Viktor Vafeiadis},
  title =	{{Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{17:1--17:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{Peter M{\"u}ller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7275},
  URN =		{urn:nbn:de:0030-drops-72753},
  doi =		{10.4230/LIPIcs.ECOOP.2017.17},
  annote =	{Keywords: Weak memory models, release-acquire, concurrency, separation logic}
}

@InProceedings{tada,
author="da Rocha Pinto, Pedro
and Dinsdale-Young, Thomas
and Gardner, Philippa",
editor="Jones, Richard",
title="{TaDA}: A Logic for Time and Data Abstraction",
booktitle="ECOOP 2014 -- Object-Oriented Programming",
year="2014",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="207--231",
abstract="To avoid data races, concurrent operations should either be at distinct times or on distinct data. Atomicity is the abstraction that an operation takes effect at a single, discrete instant in time, with linearisability being a well-known correctness condition which asserts that concurrent operations appear to behave atomically. Disjointness is the abstraction that operations act on distinct data resource, with concurrent separation logics enabling reasoning about threads that appear to operate independently on disjoint resources.",
isbn="978-3-662-44202-9"
}

@article{csl,
title = "Resources, concurrency, and local reasoning",
journal = "Theoretical Computer Science",
volume = "375",
number = "1",
pages = "271 - 307",
year = "2007",
note = "Festschrift for John C. Reynolds’s 70th birthday",
issn = "0304-3975",
doi = "https://doi.org/10.1016/j.tcs.2006.12.035",
url = "http://www.sciencedirect.com/science/article/pii/S030439750600925X",
author = "Peter W. O’Hearn",
keywords = "Concurrency, Logics of programs, Separation logic",
abstract = "In this paper we show how a resource-oriented logic, separation logic, can be used to reason about the usage of resources in concurrent programs."
}

@inproceedings{subjective,
author = {Ley-Wild, Ruy and Nanevski, Aleksandar},
title = {Subjective Auxiliary State for Coarse-Grained Concurrency},
year = {2013},
isbn = {9781450318327},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi-org.proxy.cc.uic.edu/10.1145/2429069.2429134},
doi = {10.1145/2429069.2429134},
booktitle = {Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
pages = {561–574},
numpages = {14},
keywords = {verification, local reasoning, dependent type theory, rely-guarantee thinking, concurrency},
location = {Rome, Italy},
series = {POPL ’13}
}

@article{iris-guide,
  author    = {Elizabeth Dietrich},
  title     = {A beginner guide to {Iris}, {Coq} and separation logic},
  journal   = {CoRR},
  volume    = {abs/2105.12077},
  year      = {2021},
  url       = {https://arxiv.org/abs/2105.12077},
  eprinttype = {arXiv},
  eprint    = {2105.12077},
  timestamp = {Tue, 01 Jun 2021 18:07:59 +0200},
  biburl    = {https://dblp.org/rec/journals/corr/abs-2105-12077.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{rustbelt,
    author = {Jung, Ralf and Jourdan, Jacques-Henri and Krebbers, Robbert and Dreyer, Derek},
    title = {{RustBelt}: Securing the Foundations of the Rust Programming Language},
    year = {2017},
    issue_date = {January 2018},
    publisher = {Association for Computing Machinery},
    address = {New York, NY, USA},
    volume = {2},
    number = {POPL},
    url = {https://doi.org/10.1145/3158154},
    doi = {10.1145/3158154},
    abstract = {Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust's safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power of this core type system through libraries that internally use unsafe features. In this paper, we give the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem.},
    journal = {Proc. ACM Program. Lang.},
    month = {Dec},
    articleno = {66},
    numpages = {34},
    keywords = {logical relations, type systems, Rust, concurrency, separation logic}
    }
    
@article{rustbelt-relaxed,
  author    = {Hoang{-}Hai Dang and
               Jacques{-}Henri Jourdan and
               Jan{-}Oliver Kaiser and
               Derek Dreyer},
  title     = {RustBelt meets relaxed memory},
  journal   = {Proc. {ACM} Program. Lang.},
  volume    = {4},
  number    = {{POPL}},
  pages     = {34:1--34:29},
  year      = {2020},
  url       = {https://doi.org/10.1145/3371102},
  doi       = {10.1145/3371102},
  timestamp = {Wed, 17 Feb 2021 08:54:07 +0100},
  biburl    = {https://dblp.org/rec/journals/pacmpl/DangJKD20.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{iris-vst-arxiv,
  doi = {10.48550/ARXIV.2207.06574},
  
  journal   = {CoRR},
  volume    = {abs/2207.06574},

  url = {https://arxiv.org/abs/2207.06574},
  
  author = {Mansky, William},
  
  keywords = {Programming Languages (cs.PL), FOS: Computer and information sciences, FOS: Computer and information sciences, F.3.1},
  
  title = {Bringing {Iris} into the {Verified Software Toolchain}},
  
  publisher = {arXiv},
  
  year = {2022},
  
  copyright = {Creative Commons Attribution Non Commercial Share Alike 4.0 International}
}