diff --git a/docs/algebra.tex b/docs/algebra.tex index 29c14219774d8a59db2316f0abd54099dc342d67..e6fd00b9e673228b5da8c05ee650e48657cfadd7 100644 --- a/docs/algebra.tex +++ b/docs/algebra.tex @@ -172,7 +172,7 @@ Note that for RAs, this and the RA-based definition of a frame-preserving update A CMRA $\monoid$ is \emph{discrete} if it satisfies the following conditions: \begin{enumerate}[itemsep=0pt] \item $\monoid$ is a discrete COFE - \item $\val$ ignores the step-index: \\ + \item $\mval$ ignores the step-index: \\ $\All \melt \in \monoid. \melt \in \mval_0 \Ra \All n, \melt \in \mval_n$ \end{enumerate} \end{defn} diff --git a/docs/bib.bib b/docs/bib.bib index 506c8d5f13a3ae07da79f026a5824ff706ee1437..7658e619c30367cb7d91ce10595c812cf6f8fee0 100644 --- a/docs/bib.bib +++ b/docs/bib.bib @@ -3532,6 +3532,9 @@ year = {2013} title = {Invariants, Modularity, and Rights}, booktitle = {PSI}, year = {2009}, + pages = {43--55}, + volume = {5947}, + series = {LNCS}, } @Article{ashcroft:invariants, @@ -3635,7 +3638,7 @@ year = {2013} Georges Gonthier and Assia Mahboubi and Laurence Rideau}, - title = "{Packaging Mathematical Structures}", + title = {Packaging Mathematical Structures}, booktitle = {TPHOLs}, pages = {327--342}, series = {LNCS}, @@ -3645,7 +3648,7 @@ year = {2013} @article{spitters:weegen:11, author = {Bas Spitters and Eelis van der Weegen}, - title = "{Type classes for mathematics in type theory}", + title = {Type classes for mathematics in type theory}, journal = {MSCS}, volume = {21}, number = {4}, @@ -3655,8 +3658,8 @@ year = {2013} @article{sozeau:09, author = {Matthieu Sozeau}, - title = "{A New Look at Generalized Rewriting in Type Theory}", - journal = {Journal of Formalized Reasoning}, + title = {A New Look at Generalized Rewriting in Type Theory}, + journal = {JFR}, volume = {2}, number = {1}, pages = {41--62}, @@ -3701,3 +3704,120 @@ year = {2013} biburl = {http://dblp.uni-trier.de/rec/bib/journals/tcs/BirkedalST10}, bibsource = {dblp computer science bibliography, http://dblp.org} } + +@inproceedings{gotsman:storable-locks, + author = {Alexey Gotsman and + Josh Berdine and + Byron Cook and + Noam Rinetzky and + Mooly Sagiv}, + title = {Local Reasoning for Storable Locks and Threads}, + booktitle = {APLAS}, + pages = {19--37}, + year = {2007}, + url = {http://dx.doi.org/10.1007/978-3-540-76637-7_3}, + doi = {10.1007/978-3-540-76637-7_3}, + timestamp = {Thu, 29 Nov 2007 12:28:33 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/aplas/GotsmanBCRS07}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{birkedal:storable-locks, + author = {Alexandre Buisse and + Lars Birkedal and + Kristian St{\o}vring}, + title = {Step-Indexed {Kripke} Model of Separation Logic for Storable Locks}, + journal = {ENTCS}, + volume = {276}, + pages = {121--143}, + year = {2011}, + url = {http://dx.doi.org/10.1016/j.entcs.2011.09.018}, + doi = {10.1016/j.entcs.2011.09.018}, + timestamp = {Mon, 14 Nov 2011 15:35:16 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/entcs/BuisseBS11}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{unification_hints, + author = {Andrea Asperti and + Wilmer Ricciotti and + Claudio Sacerdoti Coen and + Enrico Tassi}, + title = {Hints in Unification}, + booktitle = {TPHOLs}, + pages = {84--98}, + year = {2009}, + series = {LNCS}, + volume = {5674}, +} + +@inproceedings{bedrock, + author = {Adam Chlipala}, + title = {The {Bedrock} structured programming system: combining generative metaprogramming + and {Hoare} logic in an extensible program verifier}, + booktitle = {ICFP}, + pages = {391--402}, + year = {2013}, +} + +@inproceedings{modures, + author = {Filip Sieczkowski and Ales Bizjak and Lars Birkedal}, + title = {{ModuRes}: {A} {Coq} Library for Modular Reasoning About Concurrent Higher-Order + Imperative Programming Languages}, + booktitle = {ITP}, + pages = {375--390}, + year = {2015}, + series = {LNCS}, + volume = {9236}, +} + +@inproceedings{fcsl-coq, + author = {Ilya Sergey and + Aleksandar Nanevski and + Anindya Banerjee}, + title = {Mechanized verification of fine-grained concurrent programs}, + booktitle = {PLDI}, + pages = {77--87}, + year = {2015}, + url = {http://doi.acm.org/10.1145/2737924.2737964}, + doi = {10.1145/2737924.2737964}, + timestamp = {Fri, 05 Jun 2015 07:31:54 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/pldi/SergeyNB15}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@book{app:14, + editor = {Andrew W. Appel}, + title = "{Program Logics for Certified Compilers}", + year = {2014}, + publisher = {Cambridge University Press} +} + +@inproceedings{charge, + author = {Jesper Bengtson and Jonas Braband Jensen and Lars Birkedal}, + title = "{Charge! - {A} Framework for Higher-Order Separation Logic in {C}oq}", + booktitle = {ITP}, + year = {2012}, + pages = {315--331}, + series = {LNCS}, + volume = {7406}, +} + +@inproceedings{jensen:benton:kennedy:13, + author = {Jonas Braband Jensen and + Nick Benton and + Andrew Kennedy}, + title = {High-level separation logic for low-level code}, + booktitle = {POPL}, + pages = {301--314}, + year = {2013}, +} + +@inproceedings{tuch:klein:norrish:07, + author = {Harvey Tuch and Gerwin Klein and Michael Norrish}, + title = {Types, bytes, and separation logic}, + booktitle = {POPL}, + year = {2007}, + pages = {97--108}, +} + diff --git a/docs/iris.sty b/docs/iris.sty index f86e50a3b152932500c37086278a622a94731d36..0b5ca1b607b9c62c75df5e2d3933a361aad74250 100644 --- a/docs/iris.sty +++ b/docs/iris.sty @@ -122,7 +122,7 @@ \newcommand{\cofe}{T} \newcommand{\cofeB}{U} -\newcommand{\COFEs}{\mathcal{U}} % category of COFEs +\newcommand{\COFEs}{\mathcal{COFE}} % category of COFEs \newcommand{\iFunc}{\Sigma} \newcommand{\fix}{\textdom{fix}} @@ -151,7 +151,7 @@ \newcommand{\mupd}{\rightsquigarrow} \newcommand{\mincl}[1][]{\ensuremath{\mathrel{\stackrel{#1}{\preccurlyeq}}}} -\newcommand{\CMRAs}{\mathcal{R}} % category of CMRAs +\newcommand{\CMRAs}{\mathcal{CMRA}} % category of CMRAs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% LOGIC SYMBOLS & NOTATION & IDENTIFIERS