Docs: CMRA → Camera (as in the Ground Up paper).

docs/algebra.tex

@@ -126,7 +126,7 @@ RAs are closely related to \emph{Partial Commutative Monoids} (PCMs), with two k
 \item The composition operation on RAs is total (as opposed to the partial composition operation of a PCM), but there is a specific subset of \emph{valid} elements that is compatible with the composition operation (\ruleref{ra-valid-op}).
 These valid elements are identified by the \emph{validity predicate} $\mvalFull$.
 
-This take on partiality is necessary when defining the structure of \emph{higher-order} ghost state, CMRAs, in the next subsection.
+This take on partiality is necessary when defining the structure of \emph{higher-order} ghost state, \emph{cameras}, in the next subsection.
 
 \item Instead of a single unit that is an identity to every element, we allow
 for an arbitrary number of units, via a function $\mcore{{-}}$ assigning to an element $\melt$ its \emph{(duplicable) core} $\mcore\melt$, as demanded by \ruleref{ra-core-id}.
@@ -154,22 +154,22 @@ Notice that $\maybe{\melt_\f}$ could be $\mnocore$, so the frame-preserving upda
 Intuitively, this means that whatever assumptions the rest of the program is making about the state of $\gname$, if these assumptions are compatible with $\melt$, then updating to $\meltB$ will not invalidate any of these assumptions.
 Since Iris ensures that the global ghost state is valid, this means that we can soundly update the ghost state from $\melt$ to a non-deterministically picked $\meltB \in \meltsB$.
 
-\subsection{CMRA}
+\subsection{Cameras}
 
 \begin{defn}
-  A \emph{CMRA} is a tuple $(\monoid : \OFEs, \mval : \monoid \nfn \SProp, \mcore{{-}}: \monoid \nfn \maybe\monoid,\\ (\mtimes) : \monoid \times \monoid \nfn \monoid)$ satisfying:
+  A \emph{camera} is a tuple $(\monoid : \OFEs, \mval : \monoid \nfn \SProp, \mcore{{-}}: \monoid \nfn \maybe\monoid,\\ (\mtimes) : \monoid \times \monoid \nfn \monoid)$ satisfying:
   \begin{align*}
-    \All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{cmra-assoc} \\
-    \All \melt, \meltB.& \melt \mtimes \meltB = \meltB \mtimes \melt \tagH{cmra-comm} \\
-    \All \melt.& \mcore\melt \in \monoid \Ra \mcore\melt \mtimes \melt = \melt \tagH{cmra-core-id} \\
-    \All \melt.& \mcore\melt \in \monoid \Ra \mcore{\mcore\melt} = \mcore\melt \tagH{cmra-core-idem} \\
-    \All \melt, \meltB.& \mcore\melt \in \monoid \land \melt \mincl \meltB \Ra \mcore\meltB \in \monoid \land \mcore\melt \mincl \mcore\meltB \tagH{cmra-core-mono} \\
-    \All \melt, \meltB.& \mval(\melt \mtimes \meltB) \subseteq \mval(\melt)  \tagH{cmra-valid-op} \\
+    \All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{camera-assoc} \\
+    \All \melt, \meltB.& \melt \mtimes \meltB = \meltB \mtimes \melt \tagH{camera-comm} \\
+    \All \melt.& \mcore\melt \in \monoid \Ra \mcore\melt \mtimes \melt = \melt \tagH{camera-core-id} \\
+    \All \melt.& \mcore\melt \in \monoid \Ra \mcore{\mcore\melt} = \mcore\melt \tagH{camera-core-idem} \\
+    \All \melt, \meltB.& \mcore\melt \in \monoid \land \melt \mincl \meltB \Ra \mcore\meltB \in \monoid \land \mcore\melt \mincl \mcore\meltB \tagH{camera-core-mono} \\
+    \All \melt, \meltB.& \mval(\melt \mtimes \meltB) \subseteq \mval(\melt)  \tagH{camera-valid-op} \\
     \All n, \melt, \meltB_1, \meltB_2.& \omit\rlap{$n \in \mval(\melt) \land \melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \Ra {}$} \\
-    &\Exists \meltC_1, \meltC_2. \melt = \meltC_1 \mtimes \meltC_2 \land \meltC_1 \nequiv{n} \meltB_1 \land \meltC_2 \nequiv{n} \meltB_2 \tagH{cmra-extend} \\
+    &\Exists \meltC_1, \meltC_2. \melt = \meltC_1 \mtimes \meltC_2 \land \meltC_1 \nequiv{n} \meltB_1 \land \meltC_2 \nequiv{n} \meltB_2 \tagH{camera-extend} \\
     \text{where}\qquad\qquad\\
-    \melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{cmra-incl} \\
-    \melt \mincl[n] \meltB \eqdef{}& \Exists \meltC. \meltB \nequiv{n} \melt \mtimes \meltC \tagH{cmra-inclN}
+    \melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{camera-incl} \\
+    \melt \mincl[n] \meltB \eqdef{}& \Exists \meltC. \meltB \nequiv{n} \melt \mtimes \meltC \tagH{camera-inclN}
   \end{align*}
 \end{defn}
 
@@ -178,7 +178,7 @@ All operations have to be non-expansive, and the validity predicate $\mval$ can
 We define the plain $\mvalFull$ as the ``limit'' of the step-indexed approximation:
 \[ \mvalFull(\melt) \eqdef \All n. n \in \mval(\melt) \]
 
-\paragraph{The extension axiom (\ruleref{cmra-extend}).}
+\paragraph{The extension axiom (\ruleref{camera-extend}).}
 Notice that the existential quantification in this axiom is \emph{constructive}, \ie it is a sigma type in Coq.
 The purpose of this axiom is to compute $\melt_1$, $\melt_2$ completing the following square:
 
@@ -203,7 +203,7 @@ This operation is needed to prove that $\later$ commutes with separating conjunc
 \end{mathpar}
 
 \begin{defn}
-  An element $\munit$ of a CMRA $\monoid$ is called the \emph{unit} of $\monoid$ if it satisfies the following conditions:
+  An element $\munit$ of a camera $\monoid$ is called the \emph{unit} of $\monoid$ if it satisfies the following conditions:
   \begin{enumerate}[itemsep=0pt]
   \item $\munit$ is valid: \\ $\All n. n \in \mval(\munit)$
   \item $\munit$ is a left-identity of the operation: \\
@@ -212,7 +212,7 @@ This operation is needed to prove that $\later$ commutes with separating conjunc
   \end{enumerate}
 \end{defn}
 
-\begin{lem}\label{lem:cmra-unit-total-core}
+\begin{lem}\label{lem:camera-unit-total-core}
   If $\monoid$ has a unit $\munit$, then the core $\mcore{{-}}$ is total, \ie $\All\melt. \mcore\melt \in \monoid$.
 \end{lem}
 
@@ -225,18 +225,18 @@ This operation is needed to prove that $\later$ commutes with separating conjunc
 Note that for RAs, this and the RA-based definition of a frame-preserving update coincide.
 
 \begin{defn}
-  A CMRA $\monoid$ is \emph{discrete} if it satisfies the following conditions:
+  A camera $\monoid$ is \emph{discrete} if it satisfies the following conditions:
   \begin{enumerate}[itemsep=0pt]
   \item $\monoid$ is a discrete COFE
   \item $\mval$ ignores the step-index: \\
     $\All \melt \in \monoid. 0 \in \mval(\melt) \Ra \All n. n \in \mval(\melt)$
   \end{enumerate}
 \end{defn}
-Note that every RA is a discrete CMRA, by picking the discrete COFE for the equivalence relation.
-Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE structure, as well as the step-index of $\mval$.
+Note that every RA is a discrete camera, by picking the discrete COFE for the equivalence relation.
+Furthermore, discrete cameras can be turned into RAs by ignoring their COFE structure, as well as the step-index of $\mval$.
 
-\begin{defn}[CMRA homomorphism]
-  A function $f : \monoid_1 \to \monoid_2$ between two CMRAs is \emph{a CMRA homomorphism} if it satisfies the following conditions:
+\begin{defn}[Camera homomorphism]
+  A function $f : \monoid_1 \to \monoid_2$ between two cameras is \emph{a camera homomorphism} if it satisfies the following conditions:
   \begin{enumerate}[itemsep=0pt]
   \item $f$ is non-expansive
   \item $f$ commutes with composition:\\
@@ -249,7 +249,7 @@ Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE struct
 \end{defn}
 
 \begin{defn}
-  The category $\CMRAs$ consists of CMRAs as objects, and monotone functions as arrows.
+  The category $\CMRAs$ consists of cameras as objects, and monotone functions as arrows.
 \end{defn}
 Note that every object/arrow in $\CMRAs$ is also an object/arrow of $\OFEs$.
 The notion of a locally non-expansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.

docs/base-logic.tex

 \section{Base Logic}
 \label{sec:base-logic}
 
-The base logic is parameterized by an arbitrary CMRA $\monoid$ having a unit $\munit$.
-By \lemref{lem:cmra-unit-total-core}, this means that the core of $\monoid$ is a total function, so we will treat it as such in the following.
+The base logic is parameterized by an arbitrary camera $\monoid$ having a unit $\munit$.
+By \lemref{lem:camera-unit-total-core}, this means that the core of $\monoid$ is a total function, so we will treat it as such in the following.
 This defines the structure of resources that can be owned.
 
 As usual for higher-order logics, you can furthermore pick a \emph{signature} $\Sig = (\SigType, \SigFn, \SigAx)$ to add more types, symbols and axioms to the language.
@@ -193,7 +193,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
 	\infer{\vctx \proves \wtt{\melt}{\textlog{M}}}
 		{\vctx \proves \wtt{\ownM{\melt}}{\Prop}}
 \and
-	\infer{\vctx \proves \wtt{\melt}{\type} \and \text{$\type$ is a CMRA}}
+	\infer{\vctx \proves \wtt{\melt}{\type} \and \text{$\type$ is a camera}}
 		{\vctx \proves \wtt{\mval(\melt)}{\Prop}}
 \and
 	\infer{\vctx \proves \wtt{\prop}{\Prop}}

docs/constructions.tex

@@ -19,7 +19,7 @@ $\latert(-)$ is a locally \emph{contractive} functor from $\OFEs$ to $\OFEs$.
 
 \subsection{Uniform Predicates}
 
-Given a CMRA $\monoid$, we define the COFE $\UPred(\monoid)$ of \emph{uniform predicates} over $\monoid$ as follows:
+Given a camera $\monoid$, we define the COFE $\UPred(\monoid)$ of \emph{uniform predicates} over $\monoid$ as follows:
 \begin{align*}
 \monoid \monnra \SProp \eqdef{}& \setComp{\pred: \monoid \nfn \SProp}
 {\All n, \melt, \meltB. \melt \mincl[n] \meltB \Ra \pred(\melt) \nincl{n} \pred(\meltB)} \\
@@ -27,7 +27,7 @@ Given a CMRA $\monoid$, we define the COFE $\UPred(\monoid)$ of \emph{uniform pr
   \pred \equiv \predB \eqdef{}& \All m, \melt. m \in \mval(\melt) \Ra (m \in \pred(\melt) \iff  m \in \predB(\melt)) \\
   \pred \nequiv{n} \predB \eqdef{}& \All m \le n, \melt. m \in \mval(\melt) \Ra (m \in \pred(\melt) \iff  m \in \predB(\melt))
 \end{align*}
-You can think of uniform predicates as monotone, step-indexed predicates over a CMRA that ``ignore'' invalid elements (as defined by the quotient).
+You can think of uniform predicates as monotone, step-indexed predicates over a camera that ``ignore'' invalid elements (as defined by the quotient).
 
 $\UPred(-)$ is a locally non-expansive functor from $\CMRAs$ to $\COFEs$.
 
@@ -51,12 +51,12 @@ connective.
 
 
 \clearpage
-\section{RA and CMRA Constructions}
+\section{RA and Camera Constructions}
 
 \subsection{Product}
 \label{sec:prodm}
 
-Given a family $(M_i)_{i \in I}$ of CMRAs ($I$ finite), we construct a CMRA for the product $\prod_{i \in I} M_i$ by lifting everything pointwise.
+Given a family $(M_i)_{i \in I}$ of cameras ($I$ finite), we construct a camera for the product $\prod_{i \in I} M_i$ by lifting everything pointwise.
 
 Frame-preserving updates on the $M_i$ lift to the product:
 \begin{mathpar}
@@ -68,7 +68,7 @@ Frame-preserving updates on the $M_i$ lift to the product:
 \subsection{Sum}
 \label{sec:summ}
 
-The \emph{sum CMRA} $\monoid_1 \csumm \monoid_2$ for any CMRAs $\monoid_1$ and $\monoid_2$ is defined as (again, we use a datatype-like notation):
+The \emph{sum camera} $\monoid_1 \csumm \monoid_2$ for any cameras $\monoid_1$ and $\monoid_2$ is defined as (again, we use a datatype-like notation):
 \begin{align*}
   \monoid_1 \csumm \monoid_2 \eqdef{}& \cinl(\melt_1:\monoid_1) \mid \cinr(\melt_2:\monoid_2) \mid \mundef \\
   \mval(\mundef) \eqdef{}& \emptyset \\
@@ -82,7 +82,7 @@ Above, $\mval_1$ refers to the validity of $\monoid_1$.
 The validity, composition and core for $\cinr$ are defined symmetrically.
 The remaining cases of the composition and core are all $\mundef$.
 
-Notice that we added the artificial ``invalid'' (or ``undefined'') element $\mundef$ to this CMRA just in order to make certain compositions of elements (in this case, $\cinl$ and $\cinr$) invalid.
+Notice that we added the artificial ``invalid'' (or ``undefined'') element $\mundef$ to this camera just in order to make certain compositions of elements (in this case, $\cinl$ and $\cinr$) invalid.
 
 The step-indexed equivalence is inductively defined as follows:
 \begin{mathpar}
@@ -104,12 +104,12 @@ We obtain the following frame-preserving updates, as well as their symmetric cou
   {\All \melt_\f \in M, n. n  \notin \mval(\melt \mtimes \melt_\f) \and \mvalFull(\meltB)}
   {\cinl(\melt) \mupd \cinr(\meltB)}
 \end{mathpar}
-Crucially, the second rule allows us to \emph{swap} the ``side'' of the sum that the CMRA is on if $\mval$ has \emph{no possible frame}.
+Crucially, the second rule allows us to \emph{swap} the ``side'' of the sum that the camera is on if $\mval$ has \emph{no possible frame}.
 
 \subsection{Option}
 
-The definition of the (CM)RA axioms already lifted the composition operation on $\monoid$ to one on $\maybe\monoid$.
-We can easily extend this to a full CMRA by defining a suitable core, namely
+The definition of the camera/RA axioms already lifted the composition operation on $\monoid$ to one on $\maybe\monoid$.
+We can easily extend this to a full camera by defining a suitable core, namely
 \begin{align*}
   \mcore{\mnocore} \eqdef{}& \mnocore & \\
   \mcore{\maybe\melt} \eqdef{}& \mcore\melt & \text{If $\maybe\melt \neq \mnocore$}
@@ -119,7 +119,7 @@ Notice that this core is total, as the result always lies in $\maybe\monoid$ (ra
 \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.
+Given some infinite countable $K$ and some camera $\monoid$, the set of finite partial functions $K \fpfn \monoid$ is equipped with a camera structure by lifting everything pointwise.
 
 We obtain the following frame-preserving updates:
 \begin{mathpar}
@@ -141,7 +141,7 @@ $K \fpfn (-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$.
 
 \subsection{Agreement}
 
-Given some OFE $\cofe$, we define the CMRA $\agm(\cofe)$ as follows:
+Given some OFE $\cofe$, we define the camera $\agm(\cofe)$ as follows:
 \begin{align*}
   \agm(\cofe) \eqdef{}& \setComp{\melt \in \finpset\cofe}{\melt \neq \emptyset} /\ {\sim} \\[-0.2em]
   \melt \nequiv{n} \meltB \eqdef{}& (\All x \in \melt. \Exists y \in \meltB. x \nequiv{n} y) \land (\All y \in \meltB. \Exists x \in \melt. x \nequiv{n} y) \\
@@ -168,9 +168,9 @@ There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can
 \end{mathpar}
 
 
-\subsection{Exclusive CMRA}
+\subsection{Exclusive Camera}
 
-Given an OFE $\cofe$, we define a CMRA $\exm(\cofe)$ such that at most one $x \in \cofe$ can be owned:
+Given an OFE $\cofe$, we define a camera $\exm(\cofe)$ such that at most one $x \in \cofe$ can be owned:
 \begin{align*}
   \exm(\cofe) \eqdef{}& \exinj(\cofe) \mid \mundef \\
   \mval(\melt) \eqdef{}& \setComp{n}{\melt \neq \mundef}
@@ -276,9 +276,9 @@ We obtain the following frame-preserving update:
 
 
 \subsection{Authoritative}
-\label{sec:auth-cmra}
+\label{sec:auth-camera}
 
-Given a CMRA $M$, we construct $\authm(M)$ modeling someone owning an \emph{authoritative} element $\melt$ of $M$, and others potentially owning fragments $\meltB \mincl \melt$ of $\melt$.
+Given a camera $M$, we construct $\authm(M)$ modeling someone owning an \emph{authoritative} element $\melt$ of $M$, and others potentially owning fragments $\meltB \mincl \melt$ of $\melt$.
 We assume that $M$ has a unit $\munit$, and hence its core is total.
 (If $M$ is an exclusive monoid, the construction is very similar to a half-ownership monoid with two asymmetric halves.)
 \begin{align*}
@@ -309,7 +309,7 @@ We then obtain
 \end{mathpar}
 
 \subsection{STS with Tokens}
-\label{sec:sts-cmra}
+\label{sec:sts-camera}
 
 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.
 

docs/derived.tex

@@ -109,7 +109,7 @@ This is essentially an \emph{optional later}, indicating that the lemmas can be
 \newcommand\SliceInv{\textlog{SliceInv}}
 
 The above rules are validated by the following model.
-We need a CMRA as follows:
+We need a camera as follows:
 \begin{align*}
   \BoxState \eqdef{}& \BoxFull + \BoxEmp \\
   \BoxM \eqdef{}& \authm(\maybe{\exm(\BoxState)}) \times \maybe{\agm(\latert \iProp)}

docs/ghost-state.tex

@@ -135,7 +135,7 @@ The following rules identify the class of timeless assertions:
 {\timeless{\ownM\melt}}
 
 \infer
-{\text{$\melt$ is an element of a discrete CMRA}}
+{\text{$\melt$ is an element of a discrete camera}}
 {\timeless{\mval(\melt)}}
 \end{mathparpagebreakable}
 

docs/iris.sty

@@ -155,8 +155,8 @@
 \newcommand{\ofeB}{U}
 \newcommand{\cofe}{\ofe}
 \newcommand{\cofeB}{\ofeB}
-\newcommand{\OFEs}{\mathcal{OFE}} % category of OFEs
-\newcommand{\COFEs}{\mathcal{COFE}} % category of COFEs
+\newcommand{\OFEs}{\mathbf{OFE}} % category of OFEs
+\newcommand{\COFEs}{\mathbf{COFE}} % category of COFEs
 \newcommand{\iFunc}{\Sigma}
 \newcommand{\fix}{\textdom{fix}}
 
@@ -195,7 +195,7 @@
     $\preccurlyeq$\cr
 }}}}}
 
-\newcommand{\CMRAs}{\mathcal{CMRA}} % category of CMRAs
+\newcommand{\CMRAs}{\mathbf{Camera}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %% LOGIC SYMBOLS & NOTATION & IDENTIFIERS

docs/model.tex

@@ -29,7 +29,7 @@ For each function symbol $\sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \
 \judgment[Interpretation of assertions.]{\Sem{\vctx \proves \term : \Prop} : \Sem{\vctx} \nfn \UPred(\monoid)}
 
 Remember that $\UPred(\monoid)$ is isomorphic to $\monoid \monra \SProp$.
-We are thus going to define the assertions as mapping CMRA elements to sets of step-indices.
+We are thus going to define the assertions as mapping camera elements to sets of step-indices.
 
 \begin{align*}
 	\Sem{\vctx \proves t =_\type u : \Prop}_\venv &\eqdef

docs/program-logic.tex

@@ -8,13 +8,13 @@ So in the following, we assume that some language $\Lang$ was fixed.
 \subsection{Dynamic Composeable Higher-Order Resources}
 \label{sec:composeable-resources}
 
-The base logic described in \Sref{sec:base-logic} works over an arbitrary CMRA $\monoid$ defining the structure of the resources.
-It turns out that we can generalize this further and permit picking CMRAs ``$\iFunc(\Prop)$'' that depend on the structure of assertions themselves.
+The base logic described in \Sref{sec:base-logic} works over an arbitrary camera $\monoid$ defining the structure of the resources.
+It turns out that we can generalize this further and permit picking cameras ``$\iFunc(\Prop)$'' that depend on the structure of assertions themselves.
 Of course, $\Prop$ is just the syntactic type of assertions; for this to make sense we have to look at the semantics.
 
-Furthermore, there is a composability problem with the given logic: if we have one proof performed with CMRA $\monoid_1$, and another proof carried out with a \emph{different} CMRA $\monoid_2$, then the two proofs are actually carried out in two \emph{entirely separate logics} and hence cannot be combined.
+Furthermore, there is a composability problem with the given logic: if we have one proof performed with camera $\monoid_1$, and another proof carried out with a \emph{different} camera $\monoid_2$, then the two proofs are actually carried out in two \emph{entirely separate logics} and hence cannot be combined.
 
-Finally, in many cases just having a single ``instance'' of a CMRA available for reasoning is not enough.
+Finally, in many cases just having a single ``instance'' of a camera available for reasoning is not enough.
 For example, when reasoning about a dynamically allocated data structure, every time a new instance of that data structure is created, we will want a fresh resource governing the state of this particular instance.
 While it would be possible to handle this problem whenever it comes up, it turns out to be useful to provide a general solution.
 
@@ -23,7 +23,7 @@ The purpose of this section is to describe how we solve these issues.
 \paragraph{Picking the resources.}
 The key ingredient that we will employ on top of the base logic is to give some more fixed structure to the resources.
 To instantiate the program logic, the user picks a family of locally contractive bifunctors $(\iFunc_i : \OFEs \to \CMRAs)_{i \in \mathcal{I}}$.
-(This is in contrast to the base logic, where the user picks a single, fixed CMRA that has a unit.)
+(This is in contrast to the base logic, where the user picks a single, fixed camera that has a unit.)
 
 From this, we construct the bifunctor defining the overall resources as follows:
 \begin{align*}
@@ -31,7 +31,7 @@ From this, we construct the bifunctor defining the overall resources as follows:
   \textdom{ResF}(\ofe^\op, \ofe) \eqdef{}& \prod_{i \in \mathcal I} \GName \fpfn \iFunc_i(\ofe^\op, \ofe)
 \end{align*}
 We will motivate both the use of a product and the finite partial function below.
-$\textdom{ResF}(\ofe^\op, \ofe)$ is a CMRA by lifting the individual CMRAs pointwise, and it has a unit (using the empty finite partial functions).
+$\textdom{ResF}(\ofe^\op, \ofe)$ is a camera by lifting the individual cameras pointwise, and it has a unit (using the empty finite partial functions).
 Furthermore, since the $\iFunc_i$ are locally contractive, so is $\textdom{ResF}$.
 
 Now we can write down the recursive domain equation:
@@ -47,13 +47,13 @@ We do not need to consider how the object $\iPreProp$ is constructed, we only ne
 
 Notice that $\iProp$ is the semantic model of assertions for the base logic described in \Sref{sec:base-logic} with $\Res$:
 \[ \Sem{\Prop} \eqdef \iProp = \UPred(\Res) \]
-Effectively, we just defined a way to instantiate the base logic with $\Res$ as the CMRA of resources, while providing a way for $\Res$ to depend on $\iPreProp$, which is isomorphic to $\Sem\Prop$.
+Effectively, we just defined a way to instantiate the base logic with $\Res$ as the camera of resources, while providing a way for $\Res$ to depend on $\iPreProp$, which is isomorphic to $\Sem\Prop$.
 
 We thus obtain all the rules of \Sref{sec:base-logic}, and furthermore, we can use the maps $\wIso$ and $\wIso^{-1}$ \emph{in the logic} to convert between logical assertions $\Sem\Prop$ and the domain $\iPreProp$ which is used in the construction of $\Res$ -- so from elements of $\iPreProp$, we can construct elements of $\Sem{\textlog M}$, which are the elements that can be owned in our logic.
 
 \paragraph{Proof composability.}
 To make our proofs composeable, we \emph{generalize} our proofs over the family of functors.
-This is possible because we made $\Res$ a \emph{product} of all the CMRAs picked by the user, and because we can actually work with that product ``pointwise''.
+This is possible because we made $\Res$ a \emph{product} of all the cameras picked by the user, and because we can actually work with that product ``pointwise''.
 So instead of picking a \emph{concrete} family, proofs will assume to be given an \emph{arbitrary} family of functors, plus a proof that this family \emph{contains the functors they need}.
 Composing two proofs is then merely a matter of conjoining the assumptions they make about the functors.
 Since the logic is entirely parametric in the choice of functors, there is no trouble reasoning without full knowledge of the family of functors.
@@ -61,7 +61,7 @@ Since the logic is entirely parametric in the choice of functors, there is no tr
 Only when the top-level proof is completed we will ``close'' the proof by picking a concrete family that contains exactly those functors the proof needs.
 
 \paragraph{Dynamic resources.}
-Finally, the use of finite partial functions lets us have as many instances of any CMRA as we could wish for:
+Finally, the use of finite partial functions lets us have as many instances of any camera as we could wish for:
 Because there can only ever be finitely many instances already allocated, it is always possible to create a fresh instance with any desired (valid) starting state.
 This is best demonstrated by giving some proof rules.
 
@@ -96,7 +96,7 @@ We can show the following properties for this form of ownership:
 \end{mathparpagebreakable}
 
 Below, we will always work within (an instance of) the logic as described here.
-Whenever a CMRA is used in a proof, we implicitly assume it to be available in the global family of functors.
+Whenever a camera is used in a proof, we implicitly assume it to be available in the global family of functors.
 We will typically leave the $M_i$ implicit when asserting ghost ownership, as the type of $\melt$ will be clear from the context.
 
 
@@ -108,7 +108,7 @@ To introduce invariants into our logic, we will define weakest precondition to e
 However, in order to be able to access invariants, we will also have to provide a way to \emph{temporarily disable} (or ``open'') them.
 To this end, we use tokens that manage which invariants are currently enabled.
 
-We assume to have the following four CMRAs available:
+We assume to have the following four cameras available:
 \begin{align*}
   \InvName \eqdef{}& \nat \\
   \textmon{Inv} \eqdef{}& \authm(\InvName \fpfn \agm(\latert \iPreProp)) \\
@@ -117,7 +117,7 @@ We assume to have the following four CMRAs available:
 \end{align*}
 The last two are the tokens used for managing invariants, $\textmon{Inv}$ is the monoid used to manage the invariants themselves.
 
-We assume that at the beginning of the verification, instances named $\gname_{\textmon{State}}$, $\gname_{\textmon{Inv}}$, $\gname_{\textmon{En}}$ and $\gname_{\textmon{Dis}}$ of these CMRAs have been created, such that these names are globally known.
+We assume that at the beginning of the verification, instances named $\gname_{\textmon{State}}$, $\gname_{\textmon{Inv}}$, $\gname_{\textmon{En}}$ and $\gname_{\textmon{Dis}}$ of these cameras have been created, such that these names are globally known.
 
 \paragraph{World Satisfaction.}
 We can now define the assertion $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained: