From 3b8b2aec28e4163f43674e69b89914e847569594 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 15 Mar 2016 19:10:15 +0100 Subject: [PATCH] docs: reference Lars' metric space paper --- docs/algebra.tex | 2 + docs/bib.bib | 115 +++++++++++++++++++++++++++++++++++++++++++++++ docs/iris.sty | 5 ++- docs/model.tex | 2 +- 4 files changed, 121 insertions(+), 3 deletions(-) diff --git a/docs/algebra.tex b/docs/algebra.tex index 7d18bfab..1263d0fa 100644 --- a/docs/algebra.tex +++ b/docs/algebra.tex @@ -2,7 +2,9 @@ \subsection{COFE} +The model of Iris lives in the category of \emph{Complete Ordered Families of Equivalences} (COFEs). This definition varies slightly from the original one in~\cite{catlogic}. + \begin{defn}[Chain] Given some set $\cofe$ and an indexed family $({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \mathbb{N}}$ of equivalence relations, a \emph{chain} is a function $c : \mathbb{N} \to \cofe$ such that $\All n, m. n \leq m \Ra c (m) \nequiv{n} c (n)$. \end{defn} diff --git a/docs/bib.bib b/docs/bib.bib index 03e1cd6a..0f1f4c62 100644 --- a/docs/bib.bib +++ b/docs/bib.bib @@ -3577,3 +3577,118 @@ year = {2013} note = {Available at \url{http://users-cs.au.dk/birke/modures/tutorial/categorical-logic-tutorial-notes.pdf}} } +@article{dodds:higher-order-sync, + author = {Mike Dodds and + Suresh Jagannathan and + Matthew J. Parkinson and + Kasper Svendsen and + Lars Birkedal}, + title = {Verifying Custom Synchronization Constructs Using Higher-Order Separation + Logic}, + journal = {{ACM} Trans. Program. Lang. Syst.}, + volume = {38}, + number = {2}, + pages = {4}, + year = {2016}, + url = {http://doi.acm.org/10.1145/2818638}, + doi = {10.1145/2818638}, + timestamp = {Fri, 29 Jan 2016 12:43:32 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/toplas/DoddsJPSB16}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{iris, + author = {Ralf Jung and + David Swasey and + Filip Sieczkowski and + Kasper Svendsen and + Aaron Turon and + Lars Birkedal and + Derek Dreyer}, + title = {Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent + Reasoning}, + booktitle = {POPL}, + pages = {637--650}, + year = {2015}, +} + +@phdthesis{krebbers:phd, + author = {Robbert Krebbers}, + title = "{The C standard formalized in Coq}", + year = {2015}, + school = {Radboud University}, +} + +@inproceedings{garillot:gonthier:mahboubi:rideau:09, + author = {Fran{\c{c}}ois Garillot and + Georges Gonthier and + Assia Mahboubi and + Laurence Rideau}, + title = "{Packaging Mathematical Structures}", + booktitle = {TPHOLs}, + pages = {327--342}, + series = {LNCS}, + volume = {5674}, + year = {2009}, +} + +@article{spitters:weegen:11, + author = {Bas Spitters and Eelis van der Weegen}, + title = "{Type classes for mathematics in type theory}", + journal = {MSCS}, + volume = {21}, + number = {4}, + pages = {795--825}, + year = {2011}, +} + +@article{sozeau:09, + author = {Matthieu Sozeau}, + title = "{A New Look at Generalized Rewriting in Type Theory}", + journal = {Journal of Formalized Reasoning}, + volume = {2}, + number = {1}, + pages = {41--62}, + year = {2009}, +} + +@InProceedings{malecha:esop2016, + author = {Gregory Malecha and Jesper Bengtson}, + title = {Easy and efficient automation through reflective tactics}, + booktitle = {ESOP}, + year = 2016, +} + +@inproceedings{gps, + author = {Aaron Turon and + Viktor Vafeiadis and + Derek Dreyer}, + title = {{GPS:} navigating weak memory with ghosts, protocols, and separation}, + booktitle = {Proceedings of the 2014 {ACM} International Conference on Object Oriented + Programming Systems Languages {\&} Applications, {OOPSLA} 2014, + part of {SPLASH} 2014, Portland, OR, USA, October 20-24, 2014}, + pages = {691--707}, + year = {2014}, + url = {http://doi.acm.org/10.1145/2660193.2660243}, + doi = {10.1145/2660193.2660243}, + timestamp = {Thu, 16 Oct 2014 09:16:18 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/oopsla/TuronVD14}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{birkedal:metric-space, + author = {Lars Birkedal and + Kristian St{\o}vring and + Jacob Thamsborg}, + title = {The category-theoretic solution of recursive metric-space equations}, + journal = {Theor. Comput. Sci.}, + volume = {411}, + number = {47}, + pages = {4102--4122}, + year = {2010}, + url = {http://dx.doi.org/10.1016/j.tcs.2010.07.010}, + doi = {10.1016/j.tcs.2010.07.010}, + timestamp = {Tue, 07 Dec 2010 16:23:22 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/tcs/BirkedalST10}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} diff --git a/docs/iris.sty b/docs/iris.sty index 8b0cb49d..f86e50a3 100644 --- a/docs/iris.sty +++ b/docs/iris.sty @@ -36,7 +36,7 @@ \newcommand{\upclose}{\mathord{\uparrow}} \newcommand{\ALT}{\ |\ } -\newcommand{\spac}{\;} % a space +\newcommand{\spac}{\,} % a space \def\All #1.{\forall #1.\spac}% \def\Exists #1.{\exists #1.\spac}% @@ -292,6 +292,7 @@ %% Some commonly used identifiers \newcommand{\timeless}[1]{\textlog{timeless}(#1)} +\newcommand{\persistent}[1]{\textlog{persistent}(#1)} \newcommand{\physatomic}[1]{\textlog{atomic}($#1$)} \newcommand{\infinite}{\textlog{infinite}} @@ -362,7 +363,7 @@ \tikzstyle{sts_arrows} = [arrows={->[scale=1.5]},every node/.style={font=\sffamily\small}] %% Stored Propositions -\newcommand{\mapstoprop}{\mathrel{\mapstochar\Ra}} +\newcommand{\mapstoprop}{\mathrel{\kern-0.5ex\tikz[baseline=(m)]{\node at (0,0) (m){}; \draw[line cap=round] (0,0.16) -- (0,-0.004);}\kern-1.5ex\Ra}} \endinput diff --git a/docs/model.tex b/docs/model.tex index ea2a89bd..1fdab67f 100644 --- a/docs/model.tex +++ b/docs/model.tex @@ -60,7 +60,7 @@ Furthermore, if $F$ is locally contractive, then so is $\textdom{ResF}(-)$. Now we can write down the recursive domain equation: $\iPreProp \cong \UPred(\textdom{ResF}(\iPreProp))$ -$\iPreProp$ is a COFE, which exists by America and Rutten's theorem~\cite{America-Rutten:JCSS89}. +$\iPreProp$ is a COFE, which exists by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}. We do not need to consider how the object is constructed. We only need the isomorphism, given by \begin{align*} -- 2.24.1