update bib and irs.sty

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}

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},
+}
+

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