From d1f3cf37e8d2927910949f5857f17f7dc92d3fb1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 16 Mar 2016 13:50:29 +0100
Subject: [PATCH] update bib and irs.sty
---
docs/algebra.tex | 2 +-
docs/bib.bib | 128 +++++++++++++++++++++++++++++++++++++++++++++--
docs/iris.sty | 4 +-
3 files changed, 127 insertions(+), 7 deletions(-)
diff --git a/docs/algebra.tex b/docs/algebra.tex
index 29c142197..e6fd00b9e 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 506c8d5f1..7658e619c 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 f86e50a3b..0b5ca1b60 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
--
GitLab