diff --git a/docs/constructions.tex b/docs/constructions.tex index 0a205d8450d472dd288c9f6e4f9ddde69b5c071a..60315f69d038f7f5db84c823626ee4c583b2e97f 100644 --- a/docs/constructions.tex +++ b/docs/constructions.tex @@ -1,11 +1,11 @@ -\section{OFE and COFE constructions} +\section{OFE and COFE Constructions} -\subsection{Trivial pointwise lifting} +\subsection{Trivial Pointwise Lifting} The (C)OFE structure on many types can be easily obtained by pointwise lifting of the structure of the components. This is what we do for option $\maybe\cofe$, product $(M_i)_{i \in I}$ (with $I$ some finite index set), sum $\cofe + \cofe'$ and finite partial functions $K \fpfn \monoid$ (with $K$ infinite countable). -\subsection{Next (type-level later)} +\subsection{Next (Type-Level Later)} Given a OFE $\cofe$, we define $\latert\cofe$ as follows (using a datatype-like notation to define the type): \begin{align*} @@ -51,7 +51,7 @@ connective. \clearpage -\section{RA and CMRA constructions} +\section{RA and CMRA Constructions} \subsection{Product} \label{sec:prodm} @@ -116,7 +116,7 @@ We can easily extend this to a full CMRA by defining a suitable core, namely \end{align*} Notice that this core is total, as the result always lies in $\maybe\monoid$ (rather than in $\maybe{\mathord{\maybe\monoid}}$). -\subsection{Finite partial function} +\subsection{Finite Partial Functions} \label{sec:fpfnm} Given some infinite countable $K$ and some CMRA $\monoid$, the set of finite partial functions $K \fpfn \monoid$ is equipped with a CMRA structure by lifting everything pointwise. @@ -308,7 +308,7 @@ We then obtain {\authfull \melt_1 , \authfrag \meltB_1 \mupd \authfull \melt_2 , \authfrag \meltB_2} \end{mathpar} -\subsection{STS with tokens} +\subsection{STS with Tokens} \label{sec:sts-cmra} Given a state-transition system~(STS, \ie a directed graph) $(\STSS, {\stsstep} \subseteq \STSS \times \STSS)$, a set of tokens $\STST$, and a labeling $\STSL: \STSS \ra \wp(\STST)$ of \emph{protocol-owned} tokens for each state, we construct an RA modeling an authoritative current state and permitting transitions given a \emph{bound} on the current state and a set of \emph{locally-owned} tokens. diff --git a/docs/derived.tex b/docs/derived.tex index 13474276b789c17bccc6e7215c56fbd459908fb7..631455a88b29d7d380196b1a2ed78dfd3b023e1a 100644 --- a/docs/derived.tex +++ b/docs/derived.tex @@ -1,6 +1,6 @@ -\section{Derived constructions} +\section{Derived Constructions} -\subsection{Non-atomic (thread-local'') invariants} +\subsection{Non-Atomic (Thread-Local'') Invariants} Sometimes it is necessary to maintain invariants that we need to open non-atomically. Clearly, for this mechanism to be sound we need something that prevents us from opening the same invariant twice, something like the masks that avoid reentrancy on the normal'', atomic invariants. diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex index bd10d54efa60000c9290d79789776440300a521a..103dcfb3d7ce4575ed1630aac902c227bbe2aa16 100644 --- a/docs/ghost-state.tex +++ b/docs/ghost-state.tex @@ -3,7 +3,7 @@ In this section we discuss some additional constructions that we define within and on top of the base logic. These are not extensions'' in the sense that they change the proof power of the logic, they just form useful derived principles. -\subsection{Derived rules about base connectives} +\subsection{Derived Rules about Base Connectives} We collect here some important and frequently used derived proof rules. \begin{mathparpagebreakable} \infer{} @@ -42,7 +42,7 @@ We collect here some important and frequently used derived proof rules. Noteworthy here is the fact that $\prop \proves \later\prop$ can be derived from Löb induction, and $\TRUE \proves \plainly\TRUE$ can be derived via $\plainly$ commuting with universal quantification ranging over the empty type $0$. -\subsection{Persistent assertions} +\subsection{Persistent Assertions} We call an assertion $\prop$ \emph{persistent} if $\prop \proves \always\prop$. These are assertions that don't own anything'', so we can (and will) treat them like normal'' intuitionistic assertions. @@ -52,7 +52,7 @@ Persistence is preserved by conjunction, disjunction, separating conjunction as -\subsection{Timeless assertions and except-0} +\subsection{Timeless Assertions and Except-0} One of the troubles of working in a step-indexed logic is the later'' modality $\later$. It turns out that we can somewhat mitigate this trouble by working below the following \emph{except-0} modality: diff --git a/docs/language.tex b/docs/language.tex index f58120942900f2bc5a6f6bed1d42e03c82928804..19833fd75ab919d5747eb9affc1bf918ac807f36 100644 --- a/docs/language.tex +++ b/docs/language.tex @@ -37,7 +37,7 @@ A \emph{language} $\Lang$ consists of a set \Expr{} of \emph{expressions} (metav \end{enumerate} \end{defn} -\subsection{Concurrent language} +\subsection{Concurrent Language} For any language $\Lang$, we define the corresponding thread-pool semantics. diff --git a/docs/model.tex b/docs/model.tex index 1d9e2c74057bb0e86259e1cd510a529f52ae5298..e855482dc9d1dfd4def067f03ebf961a3c220fcb 100644 --- a/docs/model.tex +++ b/docs/model.tex @@ -1,4 +1,4 @@ -\section{Model and semantics} +\section{Model and Semantics} \label{sec:model} The semantics closely follows the ideas laid out in~\cite{catlogic}. diff --git a/docs/paradoxes.tex b/docs/paradoxes.tex index 099d1a9e7efdb9c8385c5f7ad573e994d9a4e2bf..99cdb170a15ff513308e6407e74bd6b8470c51fd 100644 --- a/docs/paradoxes.tex +++ b/docs/paradoxes.tex @@ -1,10 +1,10 @@ -\section{Logical paradoxes} +\section{Logical Paradoxes} \newcommand{\starttoken}{\textsc{s}} \newcommand{\finishtoken}{\textsc{f}} In this section we provide proofs of some logical inconsistencies that arise when slight changes are made to the Iris logic. -\subsection{Saved propositions without a later} +\subsection{Saved Propositions without a Later} \label{sec:saved-prop-no-later} As a preparation for the proof about invariants in \Sref{app:section:invariants-without-a-later}, we show that omitting the later modality from a variant of \emph{saved propositions} leads to a contradiction. @@ -75,7 +75,7 @@ With this lemma in hand, the proof of \thmref{thm:counterexample-1} is simple. Together with the rule \ruleref{sprop-alloc} we thus derive $\upd \FALSE$. \end{proof} -\subsection{Invariants without a later} +\subsection{Invariants without a Later} \label{app:section:invariants-without-a-later} Now we come to the main paradox: if we remove the $\later$ from \ruleref{inv-open}, the logic becomes inconsistent.