Commit 3b8b2aec authored by Ralf Jung's avatar Ralf Jung

docs: reference Lars' metric space paper

parent 97cfd12d
...@@ -2,7 +2,9 @@ ...@@ -2,7 +2,9 @@
\subsection{COFE} \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}. This definition varies slightly from the original one in~\cite{catlogic}.
\begin{defn}[Chain] \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)$. 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} \end{defn}
......
...@@ -3577,3 +3577,118 @@ year = {2013} ...@@ -3577,3 +3577,118 @@ year = {2013}
note = {Available at \url{http://users-cs.au.dk/birke/modures/tutorial/categorical-logic-tutorial-notes.pdf}} 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}
}
...@@ -36,7 +36,7 @@ ...@@ -36,7 +36,7 @@
\newcommand{\upclose}{\mathord{\uparrow}} \newcommand{\upclose}{\mathord{\uparrow}}
\newcommand{\ALT}{\ |\ } \newcommand{\ALT}{\ |\ }
\newcommand{\spac}{\;} % a space \newcommand{\spac}{\,} % a space
\def\All #1.{\forall #1.\spac}% \def\All #1.{\forall #1.\spac}%
\def\Exists #1.{\exists #1.\spac}% \def\Exists #1.{\exists #1.\spac}%
...@@ -292,6 +292,7 @@ ...@@ -292,6 +292,7 @@
%% Some commonly used identifiers %% Some commonly used identifiers
\newcommand{\timeless}[1]{\textlog{timeless}(#1)} \newcommand{\timeless}[1]{\textlog{timeless}(#1)}
\newcommand{\persistent}[1]{\textlog{persistent}(#1)}
\newcommand{\physatomic}[1]{\textlog{atomic}($#1$)} \newcommand{\physatomic}[1]{\textlog{atomic}($#1$)}
\newcommand{\infinite}{\textlog{infinite}} \newcommand{\infinite}{\textlog{infinite}}
...@@ -362,7 +363,7 @@ ...@@ -362,7 +363,7 @@
\tikzstyle{sts_arrows} = [arrows={->[scale=1.5]},every node/.style={font=\sffamily\small}] \tikzstyle{sts_arrows} = [arrows={->[scale=1.5]},every node/.style={font=\sffamily\small}]
%% Stored Propositions %% 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 \endinput
...@@ -60,7 +60,7 @@ Furthermore, if $F$ is locally contractive, then so is $\textdom{ResF}(-)$. ...@@ -60,7 +60,7 @@ Furthermore, if $F$ is locally contractive, then so is $\textdom{ResF}(-)$.
Now we can write down the recursive domain equation: Now we can write down the recursive domain equation:
\[ \iPreProp \cong \UPred(\textdom{ResF}(\iPreProp)) \] \[ \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 do not need to consider how the object is constructed.
We only need the isomorphism, given by We only need the isomorphism, given by
\begin{align*} \begin{align*}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment