\infer[\getrn{RTu-R}]{
\jtproc
{ \cdot }
{ \cdot }
{ \tClose{c} }
{ \cdot }
{ \focus{c : \Tu} }
{ \mc{R}_1 }
\]

Assuming every branch reaches a leaf, the axioms specify the leaf's judgment's output (the trace set in blue).
We thread these trace sets back down through the derivation tree, using the operations specified in each rule to build that rules output trace set.
In this case:

\begin{align*}
\mc{L}_1 &= \Set{ \tcons{\pO}{\mClose{b}}{\tempt} } & \mc{L}_2 &= \tcons{\pI}{\mClose{a}}{\mc{L}_1}  & & \\
\mc{R}_1 &= \Set{ \tcons{\pO}{\mClose{c}}{\tempt} } & \mc{R}_2 &= \tcons{\pC}{\mClose{a}}{\mc{R}_1} & \mc{R}_3 &= \tcons{\pI}{\mClose{b}}{\mc{R}_2}\\
\mc{L}_2 \pint \mc{R}_3 &= \mathrlap{\Set{ \tcons{\pI}{\mClose{a}}{\tcons{\pS}{\mClose{b}}{\tcons{\pO}{\mClose{c}}{\tempt}}} }} & & & &\\
\tdel{(\mc{L}_2 \pint \mc{R}_3)}{\Set{b}} &= \mathrlap{\Set{ \tcons{\pI}{\mClose{a}}{\tcons{\pO}{\mClose{c}}{\tempt}}}} &&&&
\end{align*}

Typechecking succeeds if the resulting derivation is valid (including the side condition (<ref>) for Par).

Our rules determine a terminating typechecking algorithm when all choice types are indexed by finite label sets.
Indeed, all constraint sets and their traces are finite, so trace operations terminate, and the alternating phases reduce the complexity of processes and their specifications.
Most of the typechecking complexity lies in computing operations on traces.
We conjecture that they could efficiently be implemented by representing traces as tries or radix trees.

§ SAFETY PROPERTIES

Our typechecking algorithm is sound: if we can typecheck a process against a process specification, then all executions of that process are permitted by its specification.
Put differently, our typechecking algorithm ensures that well-typed processes communicate safely:

The typechecking algorithm is sound: if any of

* \(\jtproc{\Pi}{\Iota}{P}{\Delta}{a : A}{\tfnt{T}}\),

* \(\jtred{\Pi}{\Iota}{P}{\Delta}{\focus{a : A}}{\tfnt{T}}\), or

* \(\jtred{\Pi}{\Iota}{P}{\Delta, \focus{a : A}}{c : C}{\tfnt{T}}\),

then \(\tquoc{\tfnt{T}} = \ptraces{P}\) (the set \(\tfnt{T}\) extents the executions of \(P\) with constraints) and \(\tfnt{T} \subseteq \jtts{\jwfts{\Pi}{\jwfpi{\Delta}{\Iota}{a : A}}}\) (the constraint set \(\tfnt{T}\) satisfies the specification \(\jwfts{\Pi}{\jwfpi{\Delta}{\Iota}{a : A}}\)).

By induction on the derivation.

The result is immediate by the induction hypothesis, <ref>, and <ref>.

\[
\adjustbox{max width=\linewidth}{
\getrule{Par}
\]

By the induction hypothesis, \(\tquoc{\tfnt{T}_1} = \ptraces{P}\) and \(\tquoc{\tfnt{T}_2} = \ptraces{Q}\).
By definition of \(\tfnt{T}_1 \therefore \tfnt{T}_2\),

\[
\ptraces{\tPar{a}{P}{Q}} = \ptraces{P} \pint \ptraces{Q} = (\tquoc{\tfnt{T}_1}) \pint (\tquoc{\tfnt{T}_2}) = \tquoc{(\tfnt{T}_1 \tint \tfnt{T}_2)}.
\]

The inclusion \(\tquoc{\tfnt{T}_1} \tint \tquoc{\tfnt{T}_2} \subseteq \sembr{\jwfps{\Pi}{\proci{\Delta_1, \Delta_2}{\Iota_1, a : A, \Iota_2}{c : C}}}\) is given by <ref>.

STFoc-R The result is immediate by the induction hypothesis.

STFoc-L The result is immediate by the induction hypothesis.

\[
\getrule{RTu-R}
\]

The inclusion \(\tfnt{T} = \Set{ \tcons{\pO}{\mClose{a}}{\tempt} } \subseteq \jtts{\jwfts{\Pi}{\jwfpi{\cdot}{\cdot}{a : \Tu}}}\) is easily checked.
Moreover, \(\tdel{\tfnt{T}}{\freecn(\Pi)} = \tfnt{T} = \ptraces{\tClose{a}}\) by <ref>, so we are done.

The equality is by the induction hypothesis and <ref>.
The inclusion is by the induction hypothesis and <ref>.

The equality is by the induction hypothesis and <ref>.
The inclusion is by the induction hypothesis and <ref>.

RTplus-L Analogous to RTamp-R

RTamp-L Analogous to RTplus-R.

By the induction hypothesis, \(\tquoc{\tfnt{T}_1} = \ptraces{P}\) and \(\tquoc{\tfnt{T}_2} = \ptraces{Q}\).
By <ref>,

\begin{align*}
&= \Set{ \tcons{\pO}{\mChan{a}}[b]{t} \given t_P \in \ptraces{P}, t_Q \in \ptraces{Q}, t \in t_P \pint t_Q }\\
&= \Set{ \tcons{\pO}{\mChan{a}}[b]{t} \given t_P \in \tquoc{\tfnt{T}_1}, t_Q \in \tquoc{\tfnt{T}_2}, t \in t_P \pint t_Q }\\
&= \Set{ \tcons{\pO}{\mChan{a}}[b]{t} \given t \in \tquoc{\tfnt{T}_1} \pint \tquoc{\tfnt{T}_2} }\\
\shortintertext{which by \(\getrh{RTot-R}{4}\),}
&= \Set{ \tcons{\pO}{\mChan{a}}[b]{t} \given t \in \tquoc{(\tfnt{T}_1 \tint \tfnt{T}_2)} }\\
&= \tcons{\pO}{\mChan{a}}[b]{(\tquoc{(\tfnt{T}_1 \tint \tfnt{T}_2)})}\\
&= \tquoc{(\tcons{\pO}{\mChan{a}}[b]{(\tfnt{T}_1 \tint \tfnt{T}_2)})}
\end{align*}

The desired inclusion is given by the induction hypothesis, <ref>, and <ref>.

\[
\getrule{RTlolly-R}
\]

The equality is by the induction hypothesis and <ref>.
The inclusion is by the induction hypothesis and <ref>.

RTot-L Analogous to RTlolly-R.

RTlolly-L Analogous to RTot-R.

The desired inclusion is given by the induction hypothesis and <ref>.
The desired equality is given by the induction hypothesis and <ref>.

Red-RTu, Red-LTu, Red-RTLbl, Red-LTLbl, Red-RTChan, or Red-LTChan
The inclusion is given by the induction hypothesis and the appropriate choice of <ref>.
The equality is immediate by the induction hypothesis and the definition of \(\tquoc{({-})}\).

[][all end]

If \(t \in \jtts{\jwfps{\cdot}{\mc{G}}}\), then \(\tquoc{t} = t\).

By induction on the derivation \(t \in \jtts{\jwfps{\cdot}{\mc{G}}}\).

If \(\jtproc{\cdot}{\Iota}{P}{\Delta}{a : A}{\tfnt{T}}\), then \(\tfnt{T} = \ptraces{P}\) and \(\ptraces{P} \subseteq \ptraces{\jwfps{\cdot}{\proci{\Delta}{\Iota}{a : A}}}\).

Immediate by <ref>.

A key feature of is its modular approach to process specification.
Processes whose specifications impose no constraints on their environment can always be composed:

If \(\jtproc{\cdot}{\Iota_1}{P}{\Delta_1}{a : A}{\tfnt{T}_1}\) and

\({\jtproc{\cdot}{\Iota_2}{Q}{\Delta_2, a : A}{c : C}{\tfnt{T}_2}}\),
then \(\jtproc{\cdot}{\Iota_1, a : A, \Iota_2}{\tPar{a}{P}{Q}}{\Delta_1, \Delta_2}{c : C}{\tfnt{T}_1 \pint \tfnt{T}_2}\).

* \(\jtproc{\cdot}{\Iota_1}{P}{\Delta_1}{a : A}{\tfnt{T}_1}\) and

* \(\jtproc{\cdot}{\Iota_2}{Q}{\Delta_2, a : A}{c : C}{\tfnt{T}_2}\).

By induction on the two derivations, we can weaken them to

* \(\jtproc{\Delta_2, \Iota_2, c : C}{\Iota_1}{P}{\Delta_1}{a : A}{\tfnt{T}_1}\) and

* \(\jtproc{\Delta_1, \Iota_1}{\Iota_2}{Q}{\Delta_2, a : A}{c : C}{\tfnt{T}_2}\).

To show \(\jtproc{\cdot}{\Iota_1, a : A, \Iota_2}{\tPar{a}{P}{Q}}{\Delta_1, \Delta_2}{c : C}{\tfnt{T}_1 \pint \tfnt{T}_2}\), it is sufficient by <ref> and Par to show that \(\tfnt{T}_1 \therefore \tfnt{T}_2\), , that

\[
\forall t_1 \in \tfnt{T}_1\;.\; \forall t_2 \in \tfnt{T}_2\;.\; \left(\tquoc{t_1} \pint \tquoc{t_2}\right) = \tquoc{\left(t_1 \tint t_2\right)}.
\]

Indeed, if  \(\tfnt{T}_1 \therefore \tfnt{T}_2\), then \(\jtproc{\cdot}{\Iota_1, a : A, \Iota_2}{\tPar{a}{P}{Q}}{\Delta_1, \Delta_2}{c : C}{\tfnt{T}_1 \tint \tfnt{T}_2}\) by Par.
We show that \(\tfnt{T}_1 \therefore \tfnt{T}_2\).
By <ref>, \(\tquoc{t_i} = t_i\) for all \(t_i \in \tfnt{T}_i\) with \(i = 1, 2\).
We deduce

\[
\left(\tquoc{t_1} \tint \tquoc{t_2}\right) = t_1 \tint t_2 = \tquoc{\left(t_1 \tint t_2\right)},
\]

where the last equality stems from the fact that \(\tquoc{\cdot}\) is the identity on traces with no constraints, and interleaving two traces without constraints does not introduce any constraints.
This is what we wanted to show.

§ EXTENDING

provides a foundation for the development of session-typed languages with rich specifications.
In this section, we conjecturally sketch extensions along several axes that allow to capture richer computational phenomena: selection, asynchrony, value dependency, and recursion.

§.§ Selection

Go <cit.> includes a select statement that, given a collection of communication actions to perform, randomly performs one from the set of actions that are possible.
For example, if processes \(P\) and \(Q\) attempt to communicate with a process \(R\), then process \(R\) could use a select statement to communicate with the first of the two processes that is ready.
We show how to extend with a linear variant of a select statement building on ideas from differential linear logic <cit.> and its applications to concurrency <cit.>.
Differential linear logic offers a means of adding proofs of the same sequent.
In the intuitionistic case, if we ascribe the sequents of intuitionistic linear logic with proof terms (processes), we get the rule

\[
\infer{
\Gamma \vdash P + Q :: a : A
\Gamma \vdash P :: a : A
\Gamma \vdash Q :: a : A
\]

The possible behaviours of \(P + Q\) are all those of \(P\) or \(Q\), so the sum denotes \(\sembr{P + Q} = \sembr{P} \cup \sembr{Q}\).
This clause satisfies the identities described by , namely, that process composition distributes over sums and that all processes are idempotent with regard to the sum, , that \(P + P \equiv P\) for all \(P\).
Our discussion suggests the following typing rule for sums of processes:

\[
\infer[\rn{Sum}]{
\jtproc{\Pi}{\Iota}{P_1 + P_2}{\Delta}{a : A}{\mc{T}_1 \cup \mc{T}_2}
\jtproc{\Pi}{\Iota}{P_1}{\Delta}{a : A}{\mc{T}_1}
\jtproc{\Pi}{\Iota}{P_2}{\Delta}{a : A}{\mc{T}_2}
\]

Returning to our motivating example, suppose that we want to receive channels \(a\) and \(c\) over \(b\) and \(d\), respectively, but that we do not want to impose a particular order on which of \(b\) or \(d\) is used first.
The following sum of processes receives on whichever of \(b\) or \(d\) is ready first, non-deterministically breaking any ties, and communicates over the other before continuing as \(R'\):

\[
(\tRecvC{a}{b}{\tRecvC{c}{d}{R'}}) + (\tRecvC{c}{d}{\tRecvC{a}{b}{R'}}).
\]

§.§ Asynchrony

Adapting to use an asynchronous communication semantics is straightforward, but it comes at the cost of technical complexity.
The intended semantics treats channels as unbounded FIFO buffers, where processes can always send (add a message to a buffer), and they can receive a message if one is buffered.
We implement FIFO buffers using continuation channels, where each channel carries exactly one message, and each message consists of the datum plus the name of the (continuation) channel that will carry the next message.
To preclude interference between channels, continuation channel names are globally fresh.
To illustrate, consider the trace that describes sending on \(a\) the label \(l\), receiving label \(k\), and closing \(a\).
In the synchronous setting, we simply send the three messages on \(a\), giving a trace \( \tcons{\pO}{\mLabel{a}{l}}{\tcons{\pI}{\mLabel{a}{k}}{\tcons{\pO}{\mClose{a}}{\tempt}}} \).
In the asynchronous setting, the label \(l\) is paired with a fresh name \(a_1\) when sent on \(a\); label \(k\) is paired with a fresh name \(a_2\) and sent on \(a_1\); and the close message is sent on \(a_2\).
To enforce global freshness, ensure that trace sets remain finite, and preserve compositionality, we model continuation channels in traces by bound channel names.
The corresponding trace is \( \tcons{\pO}{\mLabel{a}{l}}[a_1]{\tcons{\pI}{\mLabel{a_1}{k}}}[a_2]{\tcons{\pO}{\mClose{a_2}}{\tempt}} \), where \(a_1\) and \(a_2\) are bound.
Modifying the semantic clauses to capture asynchronous communication is then a matter of adapting the trace operations of <ref> to handle continuation channels, and of threading bindings for continuation channels throughout the semantic clauses.
For example, <ref> becomes \(\ptraces{\tSendL{a}{k}{P}} = \tcons{\pO}{\mLabel{a}{k}}[a]{ \ptraces{P} }\), where \(a\) is bound in the traces in \(\ptraces{P}\).
To type processes in the asynchronous setting, we must extend the syntax of observed communications \(\pi\) to include the name of the continuation channel, and extend type reductions \(\immred{A}{\pi}\) to substitute the continuation channel for the carrier of \(\pi\) in \(A\).
Because type reduction is localized to the operation \(\immred{A}{\pi}\) and all reductions occur in lockstep in the typing rules, we never need to worry about a continuation channel name going out of scope, and no other changes are required.

§.§ Value-dependent session types

can be extended to support value-dependent session types <cit.>, where session types can depend on values drawn from an underlying dependent functional language.
Value-dependent type formers \(\Tforall{x : \tau}{A}\) and \(\Texists{x : \tau}{A}\) respectively specify servers that receive or send values \(v\) of type \(\tau\) and then communicate according to \(\subst{v}{x}{A}\).
We first extend our syntax:

Processes  P    ⋯      aMP         Evaluate term \(M\) and send its value on \(a\)

axP       Bind received value to \(x\) in \(P\)

Session types  A    ⋯      x : τA       Dependent value receiving

x : τA      Dependent value sending

axA      Value observation

Value observation \(\TCaseV{a}{x}{A}\) observes a transmitted value \(v\) on a channel \(a\) and reduces to the type \(\subst{v}{x}{A}\).
Its reduction is defined analogously to the other immediate reductions:

\[
\immred{(\TCaseV{c}{x}{A})}{\pi} =
\begin{cases}
\subst{M}{x}{A} &\text{if }\pi = \mVal{c}{M}\\
\TCaseV{c}{x}{\immred{A}{\pi}} &\text{if }\carrcn(\pi) \neq c
\end{cases}
\]

Write \(\valof{\tau}\) for the sets of closed values of type \(\tau\).
We give meaning to value transmission by allowing terms to be embedded in traces:[Extending our semantics to capture evaluation in the underlying dependent type theory is beyond the scope of this sketch.]

\[
\ptraces{\tSendV{a}{M}{P}} = \tcons{\pO}{\mVal{a}{M}}{ \sembr{P} },
\qquad
\ptraces{\tRecvV{a}{x}{P}} = \bigcup\nolimits_{v \in \valof{\tau}} \tcons{\pI}{\mVal{a}{v}}{ \sembr{P} }.
\]
We then extend interleaving to use the underlying definitional equality on terms so that whenever \(M\) and \(v\) are definitionally equal, \((\tcons{\pO}{\mVal{a}{M}}{t_1}) \pint (\tcons{\pI}{\mVal{a}{v}}{t_2}) = \tcons{\pS}{\mVal{a}{v}}{(t_1 \pint t_2)}\)

To type processes that use values, we assume a typing judgment \(\jtypef{\Gamma}{M}{\tau}\) for the functional language and extend the process typing judgment to include \(\Gamma\).
The right process typing rules follow a similar pattern as for label transmission, and the other rules follow analogously:

ΠΙaxPΔa : x : τA⋃_v ∈τ avvxTΓ

ΠπΙπPΔπa : ATΓ, x : τ

π= ax

ΠΙaMPΔa : x : τAaMTΓ

ΠπΙπPΔπa : MxATΓ

π= aM

max width=
Π, c : (♯x : τ.C)ΙPΔa : cxA⋃_v ∈τ avvxTΓ

ΠπΙπPΔπa : ATΓ, x : τ

π= ax

♯ ∈∀, ∃

§.§ Recursion

can be extended to support mutually recursive types and processes using coinductively defined typing judgments.
We implement mutually recursive processes using process declarations \(\tDecl{f(\vec x)}{P_f}\) gathered in an implicit global context \(\Sigma_P\).
These declarations specify that the process named \(f\) is given by its implementation \(P_f\) involving channels \(\vec x\).
The syntax \(\tCall{f(\vec a)}\) calls process \(f\) with channel names \(\vec a\), and it corresponds to running \(\subst{\vec a}{\vec x}{P_f}\).
Equirecursive types are given by type declarations \(\TDecl{X[\vec x]}{A_X}\) gathered in an implicit global context \(\Sigma_A\).
Channel name variables \(\vec x\) specify the channels that \(A_X\) can observe, and \(X[\vec a]\) is definitionally equal to \(\subst{\vec a}{\vec x}{A_X}\).
A complete program \(\mathbb{P}\) is a called process name paired with explicit declarations for each called name.

Processes         P    ⋯f(a⃗)          Call named process \(f\) with channels \(\vec a\)

Session types         A    ⋯X[x⃗]      Equirecursive type names

Type declarations         Σ_A    ·Σ_A, X[x⃗]A_X      \(X[\vec x]\) is definitionally equal to \(A_X\)

Process declarations         Σ_P    ·Σ_P, f(x⃗)P_f      Process named \(f\) is implemented by \(P_f\)

Programs         ℙ    f(a⃗)Σ_P      Complete or top-level program

We assume that recursive declarations are contractive <cit.>.
This standard assumption simplifies our theory and allows us to interpret equirecursive types as regular trees.
To ensure type reduction \(\immred{A}{\pi}\) remains well defined, we interpret its definition coinductively instead of inductively.

For each fixed type \(A\), the type \(\ms{list}_A = \Tplus \Set{ \ms{nil} : \Tu, \ms{cons} : A \otimes \ms{list}_A }\) specifies lists of channels of type \(A\).
The type \( \ms{stream}_A= \Tamp \Set{ \ms{head} : A, \ms{tail} : \ms{stream}_A } \) specifies a stream of channels of type \(A\).
Given a process declaration \(\tDecl{\ms{u}(x)}{(\tRecvL{x}{\Set{\ms{head} \Rightarrow \tClose{x} \mid \ms{tail} \Rightarrow \tCall{\ms{u}(x)}}})}\), the process “\(\tCall{\ms{u}(a)}\)” is a closed process providing \(a : \ms{stream}_\Tu\).

The types \(\ms{Bits}\) and \(\ms{IdBitSeq}\ a\) and the process \(\ms{id}\) from <ref> are encoded by the following declarations, where we use the label \(\$\) and type \(\Tu\) to specify finite sequences:

\begin{align*}
\ms{Bits} &= \Tplus \Set{ \$ : \Tu, \mt{0} : \ms{Bits}, \mt{1} : \ms{Bits} }\\
\ms{IdBitSeq}[x] &= \TCaseL{x}{\{\,\$ \Rightarrow \Tplus \Set{\$: \TCaseU{x}{\Tu}}\\
&\qquad\qquad\;\mid \mt{0} \Rightarrow  \Tplus \Set{ \mt{0} : \ms{IdBitSeq}[x] } \mid \mt{1} \Rightarrow \Tplus \Set{ \mt{1} : \ms{IdBitSeq}[x] } \,\}}\\
\tDecl{\ms{id}(x,y) &}{\tRecvL{x}{\Set{\$ \Rightarrow \tWait{x}{\tClose{y}} \mid \mt{0} \Rightarrow \tSendL{y}{\mt{0}}{\tCall{\ms{id}(x,y)}} \mid \mt{1} \Rightarrow \tSendL{y}{\mt{1}}{\tCall{\ms{id}(x,y)}} }}}.
\end{align*}

We extend our semantics to support calling named processes.
Let \(\mc{P}\) be the set of declared calling interfaces \(f(\vec x)\).
A process environment is a map \(\rho : \mc{P} \to \mb{TSets}\) giving the meaning of declared processes, where \(\mb{TSets}\) is the lattice of sets of traces ordered by inclusion.
We generalize \(\sembr{P}\) from an element of \(\mb{TSets}\) to a continuous map \(\sembr{P} : (\mc{P} \to \mb{TSets}) \to \mb{TSets}\).
Calling \(f(\vec x)\) with channels \(\vec a\) means retrieving its meaning from the environment and instantiating it with the names \(\vec a\):

\[
\ptraces{\tCall{f(\vec a)}}\rho = \Set{ \subst{\vec a}{\vec x}{t} \given t \in \rho(f(\vec x)) }.
\]

We adapt the existing clauses by threading through the environments, : \( \ptraces{\tPar{a}{P}{Q}}\rho = \sembr{P}\rho \pint \sembr{Q}\rho \).
To capture parallel composition in the presence of potentially infinite traces, we must extend \(\pint\) to be a fair merge operator.
This ensures that each element from each input traces appears at a finite depth in the interleavings.
We omit the details due to space constraints.

Complete programs are processes executed in an environment where every called process name has a corresponding declaration.
Their semantics are given by

\begin{align*}
\sembr{\tProg{f(\vec a)}{\Sigma_P}} &= \sembr{\tCall{f(\vec a)}}\sembr{\Sigma_P}, \text{ where}\\
\sembr{\tDecl{f_1(\vec x_1)}{P_1}, \dotsc, \tDecl{f_n(\vec x_n)}{P_n}} &= \ms{FIX}(\lambda \rho \in (\mc{P} \to \mb{TSets}).
\left[ \rho \mid f_1(\vec x_1) \mapsto \sembr{P_1}\rho \mid \cdots \mid f_n(\vec x_n) \mapsto\sembr{P_n}\rho \right]),
\end{align*}

\(\ms{FIX}\) is the continuous fixed-point operator on \(\mc{P} \to \mb{TSets}\), and \(\left[g \mid y_1 \mapsto v_1 \mid \cdots \mid y_n \mapsto v_n\right](x)\) is \(v_i\) if \(x = y_i\) and \(g(x)\) otherwise.
Intuitively, \(\sembr{\Sigma_P}\) maps each \(f_i(\vec x_i)\) to the meaning of \(\sembr{P_i}\) in the fixed point giving meaning to the mutually recursive declarations.

If \(\Sigma_P = (\tDecl{f(x)}{\tSendL{x}{\mt{1}}{\tCall{g(x)}}}),\;\; (\tDecl{g(x)}{\tSendL{x}{\mt{0}}{\tCall{f(x)}}})\), then

\begin{align*}
\sembr{\Sigma_P} &= \ms{FIX}\left(\lambda \rho . \left[ \rho \mid f \mapsto \tcons{\pO}{\mLabel{x}{\mt{1}}}{\rho(g)} \mid g \mapsto \tcons{\pO}{\mLabel{x}{\mt{0}}}{\rho(f)} \right]\right)\\
\sembr{\tProg{f(a)}{\Sigma_P}} &= \Set{ \tcons{\pO}{\mLabel{a}{\mt{1}}}{\tcons{\pO}{\mLabel{a}{\mt{0}}}{\tcons{\pO}{\mLabel{a}{\mt{1}}}{\cdots}}} }.
\end{align*}

Process specifications still denote sets \(\sembr{\jwfps{\Pi}{\mc{G}}}\) of traces satisfying the specification.
However, to capture recursive behaviour, we adapt its definition to use a coinductively defined elementhood relation.
Elementhood is given by a coinductive reading of the rules defining \(t \in \sembr{\jwfps{\Pi}{\mc{G}}}\) generated by the obvious analogs of <ref>, :

\[
\infer{
\tcons{\pO}{\mClose{a}}{t} \in
\sembr{
\jwfts{\Pi}
{ \mc{G}
\scons
{ \cdot }
{ \cdot }
{ a : \Tu })}
t \in     \sembr{
\jwfts{\immred{\Pi}{\pi}}{ \immred{\mc{G}}{\pi} }
\pi = \mClose{a}
\quad
\infer{
\tcons{\pO}{\mLabel{a}{k}}{t} \in   \sembr{
\jwfts
{ \Pi }
{ \mc{G}
\scons
{ \Delta }
{ \Iota }
{ a : \Tplus_{l \in L} A_l })}
t \in  \sembr{
\jwfts
{ \immred{\Pi}{\pi} }
{ \immred{\mc{G}}{\pi}
\scons
{ \immred{\Delta}{\pi} }
{ \immred{\Iota}{\pi} }
{ a : A_k })}
\pi = \mLabel{a}{k}
\]

In order to type mutually recursive processes, we give our typing rules a coinductive reading and treat each component as an input to the judgment.
Then, we extend our rules with:

\[
\infer[\rn{Call}]{
\jtprocR{\Pi}{\Iota}{\tCall{f}(\vec a)}{\Delta}{c : C}{\mc{T}}
\jtprocR{\Pi}{\Iota}{\subst{\vec a}{\vec x}P_f}{\Delta}{c : C}{\mc{T}}
(\tDecl{f(\vec x)}{P_f}) \in \Sigma_P
\]

This system can be given a finitary presentation by moving from arbitrary coinductive derivations to circular derivations (finite derivations with loops) <cit.>.
We refer the reader to <cit.> for a discussion of how to do so to achieve typechecking in finite time, and also a discussion of how to encode inductive and coinductive types using value dependency and (general) equirecursive types.

§ RELATED WORK

builds on linear-logical foundations of session types pioneered by caires_pfenning_2010:_session_types_intuit_linear_propos.
Indeed, the simply typed fragment of our system is based on a proofs-as-processes interpretation of multiplicative-additive intuitionistic linear logic (MAILL), where propositions correspond to binary session types that specify communications on communication channels.
A key difference with our work is that such interpretations typically combine parallel composition and hiding into a single operation.
This is because process composition corresponds to the cut rule of linear logic.
In contrast, we have separate parallel composition and hiding operators, and we track internal channels.
This separation ensures that composition does not hide channels observed by specifications, thereby ensuring that specifications remain well-defined after process composition.
We can recover cut-style process composition with a derived rule.
Our uniform process typing system can then be seen as a conservative extension of typical interpretations of identity-free MAILL.
Another key difference is our use of focussing.
Processes can be specified with observing types, but we can only check specific communication actions (, sending a label)) against weak head normal types (, an internal choice).
This means that to type check a process, we must reduce the type of its principal channel to weak head normal form, potentially generating constraints on ambient communications along the way.
Our focussing approach ensures that we only reduce the types of principal channels.
This avoids the premature or spurious generation of constraints on ambient channels that could affect constraint compatibility in process composition, and it ensures that type checking is deterministic.

There are various dependent type systems for binary session types.
toninho_2011:_depen_session_types, toninho_yoshida_2018:_depen_session_typed_proces interpret logical quantifiers as value-dependent session types in languages with functional programming features.
As discussed in <ref>, value-dependent session types depend on transmitted functional values.
Variations include label-dependent session types <cit.>, which reify labels as a first-class type, and arithmetic refinements <cit.>, which offer type-level arithmetic using transmitted natural numbers.
Like other binary session types, value-dependent session types take a channel-local approach: a type only considers communication on a single channel.
In contrast, types in specify protocols on individual channels while potentially depending on ambient communications.

Multiparty session types <cit.> are an alternative approach to specifying systems of communicating processes.
Instead of specifying communications on individual channels, multiparty session types specify interactions between multiple parties using a global type, and then for each party project a local type specifying its interactions with the other parties.
Though multiparty session types can specify complex interactions, they are not compositional and typically require that entire systems be specified at once.
To achieve compositionality, stolze_2023:_compos_partial_multip introduced partial multiparty sessions types, which specify multiparty sessions where some parties may be missing.
Determining when partial sessions can be composed and the resulting composition is technically complex.
In contrast, is designed to ensure compositional process specifications, and the composition of process specifications is determined by a handful of inference rules.

The dynamics of processes in proofs-as-processes interpretations of intuitionistic linear logic is often given by multiset rewriting semantics <cit.>.
We instead describe the behaviour of processes using a trace semantics.
We do so to simplify relating the meaning of processes (a set of traces) with the meaning of process specifications (a set of allowed traces).
It also provides a means of ensuring that processes and specifications are mutually compatible when typechecking their composition.
We conjecture that our trace semantics captures the same observable communication behaviours <cit.> as multiset-based semantics.
It is challenging to define trace semantics or ordered semantics for process calculi with name generation or \(\alpha\)-conversion.
Some approaches, , typed event structures for \(\pi\)-calculi <cit.>, specify in advance all names that will be created; others use complex semantic composition operators involving renamings <cit.>.
In contrast, we use binding to range over all possible fresh names in a manner reminiscent of higher-order abstract syntax.
This avoids unintended name clashes when interleaving traces during process composition.
Our compact presentation also minimizes the number of traces considered by our typechecking algorithm.
Traces with binding are similar to nominal sequences <cit.>, which use a coabstraction operator to bind atoms appearing later in a sequence.
In contrast, our traces bind not atoms, but names found in later messages.
As a result, our traces more closely resemble abstract binding trees.

§ CONCLUSION

In this work we describe , a message-observing binary session type system.
It uses type-level processes to specify protocols that vary based on ambient communications. This allows us to express more precise safety guarantees that cannot be expressed by prior work.

Our main goal in designing is to ensure compositionality. We achieve this using a novel trace-based semantics that uses traces with bindings to compactly handle higher-order communications. Our main technical results are type safety and compositionality for well-typed processes.

In the future, we plan to extend with shared channels.
This would allow to capture shared data structures like shared queues, and shared services like databases.

This work was funded in part by a GS501100000038Natural Sciences and Engineering Research Council of Canadahttp://dx.doi.org/10.13039/501100000038 GS501100000038Postdoctoral Fellowship (awarded to the first author) and Discovery Grant (grant number GS501100000038206263).

§ PROOFS

Missing 'biblatex' package
The bibliography requires the 'biblatex' package.

Berlin, Germany

Springer-Verlag GmbH Germany

abstractClassical Linear Logic (CLL) has long inspired readings of its proofs as communicating processes. Wadler's CP calculus is one of these readings. Wadler gave CP an operational semantics by selecting a subset of the cut-elimination rules of CLL to use as reduction rules. This semantics has an appealing close connection to the logic, but does not resolve the status of the other cut-elimination rules, and does not admit an obvious notion of observational equivalence. We propose a new operational semantics for CP based on the idea of observing communication. We use this semantics to define an intuitively reasonable notion of observational equivalence. To reason about observational equivalence, we use the standard relational denotational semantics of CLL. We show that this denotational semantics is adequate for our operational semantics. This allows us to deduce that, for instance, all the cut-elimination rules of CLL are observational equivalences.
booktitleProgramming Languages and Systems
eventtitle26th European Symposium on Programming
eventtitleaddonESOP 2017
seriesLecture Notes in Computer Science
titleObserved Communication Semantics for Classical Processes
venueUppsala, Sweden

abstractSession-typed languages building on the Curry-Howard isomorphism between linear logic and session-typed communication guarantee session fidelity and deadlock freedom. Unfortunately, these strong guarantees exclude many naturally occurring programming patterns pertaining to shared resources. In this paper, we introduce sharing into a session-typed language where types are stratified into linear and shared layers with modal operators connecting the layers. The resulting language retains session fidelity but not the absence of deadlocks, which can arise from contention for shared processes. We illustrate our language on various examples, such as the dining philosophers problem, and provide a translation of the untyped asynchronous $\pi$-calculus into our language.
journaltitleProceedings of the ACM on Programming Languages
titleManifest Sharing With Session Types

Springer-Verlag Berlin Heidelberg

booktitleCONCUR 2010 — Concurrency Theory
eventtitle21st International Conference, CONCUR 2010
seriesLecture Notes in Computer Science
titleSession Types as Intuitionistic Linear Propositions
venueParis, France

Cambridge University Press

issuetitleBehavioural Types Part 2
journaltitleMathematical Structures in Computer Science
titleLinear Logic Propositions As Session Types

issuetitleSpecial Issue: 13th Workshop on Logic, Language, Information and Computation (WoLLIC 2006)
journaltitleInformation and Computation
titleRelating State-Based and Process-Based Concurrency Through Linear Logic (Full-Version)

Springer-Verlag Berlin Heidelberg

abstractWe propose the first compositional event structure semantics for a very expressive $\pi$-calculus, generalising Winskel's event structures for CCS. The $\pi$-calculus we model is the $\pi$I-calculus with recursive definitions and summations. First we model the synchronous calculus, introducing a notion of dynamic renaming to the standard operators on event structures. Then we model the asynchronous calculus, for which a new additional operator, called rooting, is necessary for representing causality due to new name binding. The semantics are shown to be operationally adequate and sound with respect to bisimulation.
booktitleCONCUR 2007 — Concurrency Theory
eventtitle18th International Conference on Concurrency Theory
eventtitleaddonCONCUR 2007
seriesLecture Notes in Computer Science
titleCompositional Event Structure Semantics for the Internal $\pi$-Calculus
venueLisbon, Portugal

Saarbrücken/Wadern, Germany

Schloss Dagstuhl – Leibniz-Zentrum für Informatik

abstractSession types statically prescribe bidirectional communication protocols for message-passing processes. However, simple session types cannot specify properties beyond the type of exchanged messages. In this paper we extend the type system by using index refinements from linear arithmetic capturing intrinsic attributes of data structures and algorithms. We show that, despite the decidability of Presburger arithmetic, type equality and therefore also subtyping and type checking are now undecidable, which stands in contrast to analogous dependent refinement type systems from functional languages. We also present a practical, but incomplete algorithm for type equality, which we have used in our implementation of Rast, a concurrent session-typed language with arithmetic index refinements as well as ergometric and temporal types. Moreover, if necessary, the programmer can propose additional type bisimulations that are smoothly integrated into the type equality algorithm.
booktitle31st International Conference on Concurrency Theory (CONCUR 2020)
eventtitle31st International Conference on Concurrency Theory
eventtitleaddonCONCUR 2020
seriesLeibniz International Proceedings in Informatics (LIPIcs)
titleSession Types With Arithmetic Refinements
venueVienna, Austria (Virtual Conference)

New York, New York

Association for Computing Machinery, Inc.

eventtitle38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
titleDynamic Multirole Session Types
venueAustin, Texas

abstractProof theory provides a foundation for studying and reasoning about programming languages, most directly based on the well-known Curry-Howard isomorphism between intuitionistic logic and the typed lambda-calculus. More recently, a correspondence between intuitionistic linear logic and the session-typed pi-calculus has been discovered. In this paper, we establish an extension of the latter correspondence for a fragment of substructural logic with least and greatest fixed points. We describe the computational interpretation of the resulting infinitary proof system as session-typed processes, and provide an effectively decidable local criterion to recognize mutually recursive processes corresponding to valid circular proofs as introduced by Fortier and Santocanale. We show that our algorithm imposes a stricter requirement than Fortier and Santocanale's guard condition, but is local and compositional and therefore more suitable as the basis for a programming language.
journaltitleLogical Methods in Computer Science
titleCircular Proofs As Session-Typed Processes: A Local Validity Condition
circular proofs,session types,subsingleton logic,fixed points,progress,termination,linear logic,substructural logic

issuetitleDifferential Linear Logic, Nets and Other Quantitative and Parallel Approaches to Proof-Theory
journaltitleMathematical Structures in Computer Science
titleAn Introduction To Differential Linear Logic: Proof-Nets, Models and Antiderivatives

Saarbrücken/Wadern, Germany

European Association for Computer Science Logic

Schloss Dagstuhl – Leibniz-Zentrum für Informatik

abstractOne of the authors introduced in [Santocanale, FoSSaCS, 2002] a calculus of circular proofs for studying the computability arising from the following categorical operations: finite products, finite coproducts, initial algebras, final coalgebras. The calculus presented [Santocanale, FoSSaCS, 2002] is cut-free; even if sound and complete for provability, it lacked an important property for the semantics of proofs, namely fullness w.r.t. the class of intended categorical models (called mu-bicomplete categories in [Santocanale, ITA, 2002]). In this paper we fix this problem by adding the cut rule to the calculus and by modifying accordingly the syntactical constraint ensuring soundness of proofs. The enhanced proof system fully represents arrows of the canonical model (a free mu-bicomplete category). We also describe a cut-elimination procedure as a a model of computation arising from the above mentioned categorical operations. The procedure constructs a cut-free proof-tree with possibly infinite branches out of a finite circular proof with cuts.
booktitleComputer Science Logic 2013
eventtitleComputer Science Logic 2013
seriesLeibniz International Proceedings in Informatics (LIPIcs)
titleCuts for Circular Proofs: Semantics and Cut-Elimination
venueTorino, Italy

abstractWe present a model of games based on nominal sequences, which generalise sequences with atoms and a new notion of coabstraction. This gives a new, precise, and compositional mathematical treatment of justification pointers in game semantics.
issuetitleProceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII)
journaltitleElectronic Notes in Theoretical Computer Science
titleGame Semantics in the Nominal Model

Springer-Verlag Berlin Heidelberg

eventtitle4th International Conference on Concurrency Theory
seriesLecture Notes in Computer Science
titleTypes for Dyadic Interaction
venueHildesheim, Germany

Joint European Conferences on Theory
Practice of Software, ETAPS'98

Springer-Verlag Berlin Heidelberg

abstractWe introduce basic language constructs and a type discipline as a foundation of structured communication-based concurrent programming. The constructs, which are easily translatable into the summation-less asynchronous $\pi$-calculus, allow programmers to organise programs as a combination of multiple flows of (possibly unbounded) reciprocal interactions in a simple and elegant way, subsuming the preceding communication primitives such as method invocation and rendez-vous. The resulting syntactic structure is exploited by a type discipline à la ML, which offers a high-level type abstraction of interactive behaviours of programs as well as guaranteeing the compatibility of interaction patterns between processes in a well-typed program. After presenting the formal semantics, the use of language constructs is illustrated through examples, and the basic syntactic results of the type discipline are established. Implementation concerns are also addressed.
booktitleProgramming Languages and Systems
eventtitle7th European Symposium on Programming
seriesLecture Notes in Computer Science
titleLanguage Primitives and Type Discipline for Structured Communication-Based Programming
venueLisbon, Portugal

abstractCommunication is a central elements in software development. As a potential typed foundation for structured communication-centered programming, session types have been studied over the past decade for a wide range of process calculi and programming languages, focusing on binary (two-party) sessions. This work extends the foregoing theories of binary session types to multiparty, asynchronous sessions, which often arise in practical communication-centered applications. Presented as a typed calculus for mobile processes, the theory introduces a new notion of types in which interactions involving multiple peers are directly abstracted as a global scenario. Global types retain the friendly type syntax of binary session types while specifying dependencies and capturing complex causal chains of multiparty asynchronous interactions. A global type plays the role of a shared agreement among communication peers and is used as a basis of efficient type-checking through its projection onto individual peers. The fundamental properties of the session type discipline, such as communication safety, progress, and session fidelity, are established for general n-party asynchronous interactions.
journaltitleJournal of the ACM
titleMultiparty Asynchronous Session Types

abstractPolarized SILL is a programming language that combines functional programming with session-typed message-passing concurrency. It features general recursion; code and channel transmission; and synchronous and asynchronous communication. To reason about Polarized SILL programs, we develop the first program equivalence framework based on observable communications. We give meaning to Polarized SILL programs using an observed communication semantics (OCS). Our OCS is the first to support general recursion and code transmission. We then develop a communication-based testing equivalences framework and show that one of the equivalences captured by our framework coincides with barbed congruence, the canonical notion of process equivalence. Polarized SILL's operational semantics is specified using a multiset rewriting system. We introduce fairness for multiset rewriting systems to ensure that our OCS is well-defined in the presence of non-terminating processes, and use fairness properties to simplify reasoning about processes. This work lays the foundation for observational reasoning for session-typed languages with general recursion.
journaltitleInformation and Computation
titleFairness and Communication-Based Semantics for Session-Typed Languages
Fairness,Multiset rewriting,Session types,Observed communication semantics,Testing preorders,Program equivalence

journaltitleProceedings of the ACM on Programming Languages
titleMessage-Observing Sessions

Cambridge, Massachusetts

The MIT Press

titleTypes and Programming Languages

abstractWe develop a principled integration of shared mutable state into a proposition-as-types linear logic interpretation of a session-based concurrent programming language. While the foundation of type systems for the functional core of programming languages often builds on the proposition-as-types correspondence, automatically ensuring strong safety and liveness properties, imperative features have mostly been handled by extra-logical constructions. Our system crucially builds on the integration of nondeterminism and sharing, inspired by logical rules of differential linear logic, and ensures session fidelity, progress, confluence and normalisation, while being able to handle first-class shareable reference cells storing any persistent object. We also show how preservation and, perhaps surprisingly, progress, resiliently survive in a natural extension of our language with first-class locks. We illustrate the expressiveness of our language with examples highlighting detailed features, up to simple shareable concurrent ADTs.
journaltitleProceedings of the ACM on Programming Languages
titlePropositions-As-Types and Shared State

Cham, Switzerland

abstractWe introduce CLASS, a session-typed, higher-order, core language that supports concurrent computation with shared linear state.
booktitleProgramming Languages and Systems
eventtitle32nd European Symposium on Programming
eventtitleaddonESOP 2023
seriesLecture Notes in Computer Science
titleSafe Session-Based Concurrency With Shared Linear State
venueParis, France

Saarbrücken/Wadern, Germany

Schloss Dagstuhl – Leibniz-Zentrum für Informatik

abstractIn sequential functional languages, sized types enable termination checking of programs with complex patterns of recursion in the presence of mixed inductive-coinductive types. In this paper, we adapt sized types and their metatheory to the concurrent setting. We extend the semi-axiomatic sequent calculus, a subsuming paradigm for futures-based functional concurrency, and its underlying operational semantics with recursion and arithmetic refinements. The latter enables a new and highly general sized type scheme we call sized type refinements. As a widely applicable technical device, we type recursive programs with infinitely deep typing derivations that unfold all recursive calls. Then, we observe that certain such derivations can be made infinitely wide but finitely deep. The resulting trees serve as the induction target of our strong normalization result, which we develop via a novel logical relations argument.
booktitle7th International Conference on Formal Structures for Computation and Deduction
eventtitle7th International Conference on Formal Structures for Computation and Deduction
eventtitleaddonFSCD 2022
seriesLeibniz International Proceedings in Informatics (LIPIcs)
titleType-Based Termination for Futures
venueHaifa, Israel

abstractSession types are a well-established framework for the specification of interactions between components of a distributed systems. An important issue is how to determine the type for an open system, i.e., obtained by assembling subcomponents, some of which could be missing. To this end, we introduce partial sessions and partial (multiparty) session types. Partial sessions can be composed, and the type of the resulting system is derived from those of its components without knowing any suitable global type nor the types of missing parts. To deal with this incomplete information, partial session types represent the subjective views of the interactions from participants' perspectives; when sessions are composed, different partial views can be merged if compatible, yielding a unified view of the session. Incompatible types, due to, e.g., miscommunications or deadlocks, are detected at the merging phase. In fact, in this theory the distinction between global and local types vanishes. We apply these types to a process calculus for which we prove subject reduction and progress, so that well-typed systems never violate the prescribed constraints. In particular, we introduce a generalization of the progress property, in order to accommodate the case when a partial session cannot progress not due to a deadlock, but because some participants are still missing. Therefore, partial session types support the development of systems by incremental assembling of components.
journaltitleSoftware and Systems Modeling
titleComposable Partial Multiparty Session Types for Open Systems

Springer-Verlag Berlin Heidelberg

booksubtitleParallel Architectures and Languages Europe
eventtitle6th International PARLE Conference
seriesLecture Notes in Computer Science
titleAn Interaction-Based Language and Its Typing System
venueAthens, Greece
family=The Go Project,

noteLanguage version go1.22
titleThe Go Programming Language Specification

abstractSession types have emerged as a typing discipline for communication protocols. Existing calculi with session types come equipped with many different primitives that combine communication with the introduction or elimination of the transmitted value. We present a foundational session type calculus with a lightweight operational semantics. It fully decouples communication from the introduction and elimination of data and thus features a single communication reduction, which acts as a rendezvous between senders and receivers. We achieve this decoupling by introducing label-dependent session types, a minimalist value-dependent session type system with subtyping. The system is sufficiently powerful to simulate existing functional session type systems. Compared to such systems, label-dependent session types place fewer restrictions on the code. We further introduce primitive recursion over natural numbers at the type level, thus allowing to describe protocols whose behaviour depends on numbers exchanged in messages. An algorithmic type checking system is introduced and proved equivalent to its declarative counterpart. The new calculus showcases a novel lightweight integration of dependent types and linear typing, with has uses beyond session type systems.
journaltitleProceedings of the ACM on Programming Languages
titleLabel-Dependent Session Types

New York, New York

Association for Computing Machinery, Inc.

eventtitle13th International ACM SIGPLAN Symposium on Principles and Practices of Declarative Programming
titleDependent Session Types Via Intuitionistic Linear Type Theory
venueOdense, Denmark

Cham, Switzerland

European Joint Conferences on Theory
Practice of Software

booktitleFoundations of Software Science and Computation Structures
eventtitle21st International Conference, FOSSACS 2018
seriesLecture Notes in Computer Science
titleDepending on Session-Typed Processes
venueThessaloniki, Greece

abstractWe propose a typing system for the true concurrent model of event structures that guarantees the interesting behavioural properties known as conflict freeness and confusion freeness. Conflict freeness is the true concurrent version of the notion of confluence. A system is confusion free if nondeterministic choices are localised and do not depend on the scheduling of independent components. Ours is the first typing system to control behaviour in a true concurrent model. To demonstrate its applicability, we show that typed event structures give a semantics of linearly typed version of the -calculi with internal mobility. The semantics we provide is the first event structure semantics of the -calculus and generalises Winskel's original event structure semantics of CCS.
issuetitleMathematical Foundations of Programming Semantics (MFPS 2006)
journaltitleTheoretical Computer Science
titleTyped Event Structures and the Linear $\pi$-calculus
event structures,types,linearity,confusion freeness,$\pi$-calculus

Cambridge University Press

journaltitleJournal of Functional Programming
titlePropositions As Sessions


# A Gaussian free field approach to the natural parametrisation of
$\mathrm{SLE}_{4}$

Vlad Margarint and Lukas Schoug

(September 3, 2024)

###### Abstract

We construct the natural parametrisation of $\mathrm{SLE}_{4}$ using the
Gaussian free field, complementing the corresponding results for
$\mathrm{SLE}_{\kappa}$ for $\kappa\in(0,4)$ by Benoist [2] and for
$\kappa\in(4,8)$ by Miller and Schoug [15].

##  1 Introduction

The Schramm-Loewner evolution, $\mathrm{SLE}_{\kappa}$ ($\kappa>0$),
introduced in [20] is a one-parameter family of random conformally invariant
curves which arise as the scaling limits of statistical mechanics models in
two dimensions. When constructing $\eta\sim\mathrm{SLE}_{\kappa}$ via the
Loewner differential equation (see Section 2.2), the curve is parametrised by
capacity, that is, if $K_{t}$ is the set of points in $\mathbb{H}$ which are
separated from $\infty$ by $\eta([0,t])$, then $\mathrm{hcap}(K_{t})=2t$ for
each $t\geq 0$. However, there are other parametrisations which may be equally
natural for $\mathrm{SLE}$. One example is the so-called _natural
parametrisation_ of $\mathrm{SLE}$, constructed in [12] for
$\kappa<4(7-\sqrt{33})$ and then in [14] for all $\kappa<8$. This is the
parametrisation which is conjectured to arise when considering
$\mathrm{SLE}_{\kappa}$ as a scaling limit of a discrete model where the
discrete interface is parametrised by the number of vertices it traverses (so
far this has only been proved to be the case when considering the scaling
limit of loop-erased random walk [13] and critical site percolation on the
triangular lattice [5]). It turns out that the natural parametrisation of
$\mathrm{SLE}_{\kappa}$ is in fact (a deterministic constant times) the
$d_{\kappa}$-dimensional Minkowski content of $\mathrm{SLE}_{\kappa}$, where
$d_{\kappa}=1+\kappa/8$ is the almost sure Hausdorff dimension of
$\mathrm{SLE}_{\kappa}$ [1].

In [2] the natural parametrisation of $\mathrm{SLE}_{\kappa}$ for
$\kappa\in(0,4)$ was constructed using the Gaussian free field (GFF). More
precisely, it was constructed as a conditional expectation of a certain
quantum length measure on $\mathrm{SLE}_{\kappa}$. The same was done in [15]
in the case of $\kappa\in(4,8)$, when the curves are non-simple. The goal of
this paper is to complete this picture by providing the corresponding
construction in the case $\kappa=4$. The difference in this case compared to
$\kappa\neq 4$, is that in order to cut and weld Liouville quantum gravity
(LQG) surfaces with $\eta\sim\mathrm{SLE}_{4}$, one must choose the LQG
parameter $\gamma=2$, which is the critical value. When working with critical
LQG, the calculations turn out to be a bit more cumbersome (due to the factor
containing the logarithm in the definition, see (5)) and one has to be extra
careful, as the LQG boundary length of a (Euclidean) bounded interval no
longer has finite expectation.

For a simply connected domain $D$, denote by $r_{D}(z)$ the conformal radius
of $D$ as seen from $z\in D$.

######  Theorem 1.1.

Let $\eta\sim\mathrm{SLE}_{4}$ and $(f_{t})$ be its centred Loewner chain. Let
$h^{0}$ be a zero-boundary GFF on $\mathbb{H}$ independent of $\eta$ and for
each $t>0$, define $h^{t}=h^{0}\circ f_{t}^{-1}+2\log|(f_{t}^{-1})^{\prime}|$.
We define the measure $\mu^{0}$ on $\eta$ by

$\displaystyle\mu^{0}|_{\eta([0,t])}(dz)=F(z)\mathbb{E}[\nu_{h^{t}}\,|\,\eta]\circ
f_{t}(dz),$

where $F(z)=r_{\mathbb{H}}(z)^{-1/2}$ and $\nu_{h^{t}}$ is the critical LQG
boundary length measure with respect to $h^{t}$ (see (5)). Then, there exists
a (deterministic) constant $C>0$ such that a.s. $C\mu^{0}$ is the natural
parametrisation of $\eta$.

### Related work

There have been many results concerning natural measures on random fractals.
We already mentioned the results on the natural parametrisation of
$\mathrm{SLE}$ in [12, 14, 10, 2, 15]. Moreover, in [15], a natural
conformally covariant measure on $\mathrm{CLE}_{\kappa}$, $\kappa\in(8/3,8)$,
was constructed and proved to be unique (up to multiplicative constant).
Moreover, in [3], natural conformally covariant measures on several fractals
(cut points and boundary touching points of $\mathrm{SLE}_{\kappa}$,
$\kappa>4$, $\mathrm{CLE}$ pivotal points and carpet/gasket) were constructed
and in [9] the natural measure on cut points of $\mathrm{SLE}_{\kappa}$ for
$\kappa>4$ was studied further and proved to have bounded moments.

Another related result is the construction of a family of random measures on
the so-called two-valued sets (TVS) of the GFF, carried out in [19]. This is
done similarly to the measures above, using the imaginary multiplicative chaos
(that is, a version of LQG where the real parameter $\gamma$ is replaced by
$i\sigma$ for some $\sigma\in(0,\sqrt{2})$) and it was shown that if the
conformal Minkowski contents of the TVS exist, then they are equal (up to
deterministic constants) to the constructed measures.

### Outline

Section 2 contains the necessary preliminaries and in Section 3 we prove the
main theorem. The latter section begins with the proof of the consistency of
the definition of $\mu^{0}$ for different $t>0$, after which the rest of the
section is divided into two subsections. In Section 3.1 we prove that
$\mu^{0}$ is almost surely locally finite as a measure on $\mathbb{H}$ and in
Section 3.2 we prove that $\mu^{0}$ is conformally covariant and use this
together with the local finiteness of $\mu^{0}$ on $\mathbb{H}$ to deduce the
local finiteness of $\mu^{0}$ as a measure on $\mathrm{SLE}_{4}$. The main
result then follows.

### Notation

For any quantities $a,b$, we write $a\lesssim b$ to mean $a\leq Cb$ for some
constant $C>0$ which does not depend on any of the parameters of interest.
Moreover, we write $a\gtrsim b$ if $b\lesssim a$. Finally, we write $a\asymp
b$ if $a\lesssim b$ and $a\gtrsim b$.

We denote by $\mathbb{R}$ the real line and $\mathbb{C}$ the complex plane.
Moreover, we write $\mathbb{H}$ for the upper half-plane
$\\{z\in\mathbb{C}\colon\mathrm{Im}(z)>0\\}$ and $\mathbb{D}$ for the unit
disk $\\{z\in\mathbb{C}\colon|z|<1\\}$.

We denote two-dimensional Lebesgue measure by $dz$.

### Acknowledgements

We thank Hao Wu for valuable input and an anonymous referee for helpful
comments. LS was supported by the Finnish Academy Centre of Excellence FiRST
and the ERC starting grant 804166 (SPRS).

##  2 Preliminaries

###  2.1 Random measures

A random measure is a random element in a space of measures on some Borel
space, in our case $\mathbb{C}$. For a random measure $\xi$, we define the
intensity $\mathbb{E}[\xi]$ of $\xi$ by
$\mathbb{E}[\xi](A)=\mathbb{E}[\xi(A)]$ for all Borel sets
$A\subset\mathbb{C}$. Moreover, for a $\sigma$-algebra $\mathscr{G}$, we
define the conditional intensity of $\xi$ given $\mathscr{G}$ to be the random
measure given by
$\mathbb{E}[\xi\,|\,\mathscr{G}](A)=\mathbb{E}[\xi(A)\,|\,\mathscr{G}]$ for
each Borel set $A\subset\mathbb{C}$. For more on random measures, see [7]
(note that while they require local finiteness as a part of the definition,
this property will be shown to hold for the measure we construct).

###  2.2 Schramm-Loewner evolution

Consider the Loewner differential equation

$\displaystyle\partial_{t}g_{t}(z)=\frac{2}{g_{t}(z)-W_{t}},\quad g_{0}(z)=z,$
(1)

with $W_{t}=\sqrt{\kappa}B_{t}$ where $\kappa>0$ and $B_{t}$ is a standard
Brownian motion. There exists a solution $g_{t}(z)$ to (1) for each time
$t\in[0,T_{z})$ where $T_{z}=\inf\\{t\geq 0\colon g_{t}(z)-W_{t}=0\\}$. We let
$K_{t}=\\{z\in\mathbb{H}\colon T_{z}\leq t\\}$ and note that $(g_{t})_{t\geq
0}$ is a family of conformal maps $g_{t}\colon\mathbb{H}\setminus
K_{t}\to\mathbb{H}$ such that $\lim_{z\to\infty}g_{t}(z)-z=0$, called the
$\mathrm{SLE}_{\kappa}$ Loewner chain. By [17] (for $\kappa\neq 8$) and [11]
(for $\kappa=8$) there exists a continuous curve $\eta$ such that $K_{t}$ is
the set of points separated from infinity by $\eta([0,t])$. This curve $\eta$
is an $\mathrm{SLE}_{\kappa}$ in $\mathbb{H}$ from $0$ to $\infty$. The
behaviour of $\eta$ is heavily influenced by the value of $\kappa$: if
$\kappa\leq 4$, $\eta$ is a.s. simple, if $\kappa\in(4,8)$, $\eta$ a.s.
intersects its past as well as the boundary and if $\kappa\geq 8$, the $\eta$
is a.s. space-filling. It turns out that $\eta$ has a.s. Hausdorff dimension
$d_{\kappa}=1+\kappa/8$ for $\kappa\in(0,8)$, see [1].

Denote by $(f_{t})_{t\geq 0}$ the centred Loewner chain of
$\eta\sim\mathrm{SLE}_{\kappa}$, that is, for each $t\geq 0$ and all
$z\in\mathbb{H}$, $f_{t}(z)=g_{t}(z)-W_{t}$. An important property of
$\mathrm{SLE}$ is that the law of $\eta$ is scale invariant and satisfies the
domain Markov property, that is, for any a.s. finite stopping time $\tau$, the
law of $\eta^{\tau}(u)=f_{\tau}(\eta(\tau+u))$ is $\mathrm{SLE}_{\kappa}$.

####  2.2.1 Natural parametrisation of $\mathrm{SLE}$

We now recall some basic facts about the natural parametrisation of
$\mathrm{SLE}$. The natural parametrisation of $\mathrm{SLE}$ was constructed
in [12, 14] and in [10] shown to be equal to (a deterministic constant times)
the Minkowski content of $\mathrm{SLE}$ which they also proved exists (we
shall discuss briefly what this means below). We recall that the
$d$-dimensional Minkowski content of a set $A\subset\mathbb{H}$ is (if it
exists) defined as the limit

$\displaystyle\mathrm{Cont}_{d}(A)=\lim_{r\to
0}r^{d-2}\mathrm{Area}(\\{z\in\mathbb{H}\colon\mathrm{dist}(z,A)\leq r\\}).$

For $\eta\sim\mathrm{SLE}_{\kappa}$ we let $\mathcal{M}$ denote the
$d_{\kappa}$-dimensional Minkowski content of $\eta$ (where
$d_{\kappa}=1+\kappa/8$), that is, $\mathcal{M}$ is the measure
$\mathcal{M}(D)=\mathrm{Cont}_{d_{\kappa}}(\eta\cap D)$. Typically, the
Minkowski content of $\mathrm{SLE}$ is viewed as a parametrisation of $\eta$,
that is, one can parametrise $\eta$ so that $\mathcal{M}(\eta([s,t]))=t-s$ for
all $0<s<t$.

Furthermore, it is proved that if we denote by $(f_{t})$ the centred Loewner
chain for $\eta$, then

$\displaystyle\mathbb{E}[\mathcal{M}(D)]=\int_{D}G_{\kappa}(z)dz,\quad\mathbb{E}[\mathcal{M}(D)^{2}]=\iint_{D^{2}}G_{\kappa}(z,w)dzdw,$
$\displaystyle\mathbb{E}[\mathcal{M}(D)\,|\,\eta([0,t])]=\mathcal{M}|_{\eta([0,t])}(D)+\int_{D}|f_{t}^{\prime}(z)|^{2-d}G_{\kappa}(f_{t}(z))dz,$

where $G_{\kappa}(z)=c_{\kappa}\sin^{\tfrac{8}{\kappa}-1}(\arg
z)\mathrm{Im}(z)^{d-2}$ and $c_{\kappa}>0$ and

$\displaystyle G_{\kappa}(z,w)=\lim_{r\to
0}r^{2(d-2)}\mathbb{P}(\mathrm{dist}(z,\eta)\leq r,\ \mathrm{dist}(w,\eta)\leq
r).$

Next, we recall a characterisation of the natural parametrisation which we
will use to identify the measure that we will construct with the natural
parametrisation. Again, let $(f_{t})$ be the centred Loewner chain of
$\eta\sim\mathrm{SLE}_{\kappa}$ and for each $t>0$, let $\psi_{t}=f_{t}^{-1}$.
For each $t>0$, we define the “unzipped” curve $\eta^{t}$ by

$\displaystyle\eta^{t}(u)=f_{t}(\eta(t+u)),\quad u>0,$ (2)

write $\eta^{0}=\eta$ and recall that $\eta^{t}\sim\mathrm{SLE}_{\kappa}$.
Moreover, for a $d_{\kappa}$-dimensional volume measure $\mu$ on $\eta$, we
define

$\displaystyle\mu^{t}(dz)=|\psi_{t}(z)|^{-d_{\kappa}}\mu\circ\psi_{t}(dz),$
(3)

and note that $\mu^{0}=\mu$. The following uniqueness result was proved in
[12].

######  Theorem 2.1.

Fix $\kappa\in(0,8)$, set $d_{\kappa}=1+\kappa/8$, let
$\eta\sim\mathrm{SLE}_{\kappa}$ and let $\mu$ be an a.s. locally finite
measure on $\eta$. If $(\mu^{t},\eta^{t})\overset{d}{=}(\mu,\eta)$ for all
$t\geq 0$, then there is a deterministic constant $C>0$ such that $C\mu$ is
the natural parametrisation of $\eta$.

###  2.3 Gaussian free field

Let $D$ be a Jordan domain and let $H_{0}(D)$ be the Hilbert space closure of
the space $C_{0}^{\infty}(D)$ of smooth functions with support compactly
contained in $D$, under the Dirichlet inner product

$\displaystyle(f,g)_{\nabla}=\frac{1}{2\pi}\int_{D}\nabla f(z)\cdot\nabla
g(z)dz.$

Let $(\phi_{n})_{n\geq 1}$ be an orthonormal basis of $H_{0}(D)$ and consider
a sequence $(\alpha_{n})_{n\geq 1}$ of i.i.d. $N(0,1)$ random variables. The
zero-boundary GFF $h$ on $D$ is defined by the sum $h=\sum_{n\geq
1}\alpha_{n}\phi_{n}$. The law of $h$ does not depend on the choice of
orthonormal basis and it is conformally invariant in the sense that if
$\varphi\colon\widetilde{D}\to D$ is a conformal map, then
$\widetilde{h}=h\circ\varphi$ is a zero-boundary GFF in $\widetilde{D}$.

The zero-boundary GFF satisfies a domain Markov property. Indeed, if $U\subset
D$ is open, then we have the orthogonal decomposition $H_{0}(D)=H_{0}(U)\oplus
H_{0}^{\perp}(U)$, where $H_{0}^{\perp}(U)$ is the space of functions $f\in
H_{0}(D)$ which are harmonic on $U$. It follows that we can decompose $h$ as
$h=h_{U}+h_{U}^{\perp}$, where $h$ is a zero-boundary GFF on $U$ and
$h_{U}^{\perp}$ is a distribution which agrees with $h$ on $D\setminus U$, is
harmonic on $U$ and is independent of $h_{U}$. We think of
$h_{U}^{\perp}|_{U}$ as the harmonic extension of the the values of $h$ on
$\partial U$ to $U$. With this in mind, one can also define a GFF with
boundary data $F$ as $h+f$, where $f$ is the harmonic extension of $F$ to $D$.

One can, equivalently, define the zero-boundary GFF as a centred Gaussian
process $h:H_{0}(D)\to L^{2}(D)$ with correlation kernel given by the
Dirichlet Green’s function for $D$. This means that $(h,f)$, $f\in H_{0}(D)$,
is a collection of centred Gaussians with covariance given by
$\mathbb{E}[(h,f)(h,g)]=\int_{D\times D}f(z)G_{D}(z,w)g(w)dzdw$, where $G_{D}$
is the Green’s function on $D$ for Dirichlet boundary data.

We let $H(D)$ denote the Hilbert space closure of the set of functions $f\in
C^{\infty}(D)$ with $(f,f)_{\nabla}<\infty$ such that $\int_{D}fdz=0$ (we do
not require that the functions have compact support), with respect to
$(\cdot,\cdot)_{\nabla}$. A free boundary GFF is defined in the same way as a
zero-boundary GFF, with an orthonormal basis of $H(D)$ replacing that of
$H_{0}(D)$. Similarly, the law of the free boundary GFF is independent of the
choice of orthonormal basis and it is conformally invariant.

In the interior of the domain, the laws of a zero-boundary GFF and a free
boundary GFF are mutually absolutely continuous. In fact, we may decompose a
free boundary GFF $h^{f}$ as $h^{f}=h^{0}+\mathfrak{h}$, where $h^{0}$ is a
zero-boundary GFF and $\mathfrak{h}$ is a harmonic function, independent of
$h^{0}$.

######  Remark 2.2 (Radial/lateral decomposition in $\mathbb{H}$).

We have the orthogonal decomposition
$H(\mathbb{H})=H_{\mathrm{R}}(\mathbb{H})\oplus H_{\mathrm{L}}(\mathbb{H})$,
where $H_{\mathrm{R}}(\mathbb{H})$ (resp. $H_{\mathrm{L}}(\mathbb{H})$) is the
space of functions in $H(\mathbb{H})$ which are constant (resp. has mean zero)
on each semicircle $\partial B(0,s)$.

If $h$ is a free boundary GFF on $\mathbb{H}$, then the projection of $h$ onto
$H_{\mathrm{R}}(\mathbb{H})$ is called the radial part of $h$ and if
$h_{\mathrm{R}}(z)=h_{|z|}(0)$ denotes the average value of $h$ on $\partial
B(0,|z|)$, then $(h_{\mathrm{R}}(e^{-t}))_{t\in\mathbb{R}}$ has the same law
as $(B_{2t})_{t\in\mathbb{R}}$ where $B$ is a two-sided Brownian motion with
$B_{0}=0$. The projection of $h$ onto $H_{\mathrm{L}}(\mathbb{H})$ is called
the lateral part of $h$.

###  2.4 Liouville quantum gravity

Fix $\gamma\in(0,2]$. A $\gamma$-Liouville quantum gravity ($\gamma$-LQG)
surface is a law on equivalence classes of pairs $(D,h)$ where $D$ is a simply
connected domain and $h$ a distribution on $D$, such that $(D,h)$ and
$(\widetilde{D},\widetilde{h})$ are equivalent if there exist a conformal map
$\psi\colon\widetilde{D}\to D$ such that

$\displaystyle\widetilde{h}=h\circ\psi+Q_{\gamma}\log|\psi^{\prime}|,\quad
Q_{\gamma}=\frac{2}{\gamma}+\frac{\gamma}{2}.$ (4)

Typically, $h$ is a random distribution which looks locally like a GFF. One
can also define quantum surfaces with marked points. We say that
$(D,h,z_{1},\dots,z_{n})$ and
$(\widetilde{D},\widetilde{h},\widetilde{z}_{1},\dots,\widetilde{z}_{n})$ are
equivalent if $(D,h)$ and $(\widetilde{D},\widetilde{h})$ are equivalent as
quantum surfaces and $\psi(\widetilde{z}_{j})=z_{j}$ for all $1\leq j\leq n$.

An LQG surface comes naturally equipped with an area measure and a length
measure, but we shall only need the latter. Consider a $2$-LQG surface
embedded into $\mathbb{H}$ and for $\varepsilon>0$ and $x\in\mathbb{R}$, we
denote by $h_{\varepsilon}(x)$ the average value of $h$ on $\partial
B(x,\varepsilon)\cap\mathbb{H}$ (this makes sense for any $h$ which is locally
absolutely continuous with respect to a GFF). Then we define the boundary
length measure to be

$\displaystyle\nu_{h}(dx)=\lim_{\varepsilon\to
0}\varepsilon\\!\left(\log(1/\varepsilon)-\frac{h_{\varepsilon}(x)}{2}\right)\\!e^{h_{\varepsilon}(x)}dx.$
(5)

By the conformal coordinate change (4) one can then define the quantum length
of boundaries in arbitrary simply connected domains. We note that while
$\nu_{h}$ is a measure on $\partial D$, it can actually be used to measure the
length of curves inside on $D$ as well. Indeed, if $\eta$ is a curve in $D$
and $f\colon D\setminus\eta\to D$ is a conformal map which extends to the
boundary (in the sense of prime ends), then letting $\eta^{L}$ (resp.
$\eta^{R}$) denote the left (resp. right) side of $\eta$ we define the length
of $\eta^{q}$ as $\nu_{\widetilde{h}}(f(\eta^{q}))$, where
$\widetilde{h}=h\circ f^{-1}+2\log|(f^{-1})^{\prime}|$ and $q\in\\{L,R\\}$
(note here that $Q_{2}=2$).

Next, we recall the definition of a quantum wedge.

######  Definition 2.3.

A $(\gamma,\alpha)$-quantum wedge, $\alpha\in(-\infty,Q_{\gamma})$ is a doubly
marked $\gamma$-LQG surface $\mathcal{W}=(\mathbb{H},h,0,\infty)$ such that
the projection $h_{\mathrm{L}}$ of $h$ on $H_{\mathrm{L}}(\mathbb{H})$ has the
law of the lateral part of a free boundary GFF on $\mathbb{H}$ and such that
if $X_{t}$ denotes the average value of $h$ on $\partial B(0,e^{-t})$, then
$X$ is as follows.

  * •

$(X_{t})_{t\geq 0}$ has the law of $(B_{2t}+\alpha t)_{t\geq 0}$, where $B$ is
a standard Brownian motion with $B_{0}=0$, conditioned so that $B_{2t}+\alpha
t\leq Q_{\gamma}t$ for all $t\geq 0$.

  * •

$(X_{t})_{t\leq 0}$ has the law of $(\widehat{B}_{-2t}+\alpha t)_{t\leq 0}$,
where $\widehat{B}$ is a standard Brownian motion with $\widehat{B}_{0}=0$.

  * •

$h_{\mathrm{L}}$, $(X_{t})_{t\leq 0}$ and $(X_{t})_{t\geq 0}$ are independent.

We then write
$(\mathbb{H},h,0,\infty)\sim\mathsf{QWedge}_{\bm{\gamma}=\gamma}^{\bm{\alpha}=\alpha}$.
The particular embedding in this definition is called the last exit
parametrisation.

######  Remark 2.4.

Sometimes it is useful to parametrise a quantum wedge by the strip instead.
This is done using the conformal coordinate change (4) with $\psi(z)=e^{-z}$.
Then, a last exit parametrisation embedding of
$(h,\mathscr{S},-\infty,+\infty)$ can be sampled by letting
$h=X+h_{\mathrm{L}}$ where $h_{\mathrm{L}}$, the projection of $h$ onto
$H_{\mathrm{L}}(\mathscr{S})$, has the law of the lateral part of a free
boundary GFF in $\mathscr{S}$ and $X_{t}$ is the average value of $h$ on
$\\{t\\}\times[0,\pi]$, defined as follows.

  * •

$(X_{t})_{t\geq 0}$ has the law of $(B_{2t}-(Q_{\gamma}-\alpha)t)_{t\geq 0}$,
where $B$ is a standard Brownian motion with $B_{0}=0$, conditioned so that
$B_{2t}-(Q_{\gamma}-\alpha)t\leq 0$ for all $t\geq 0$.

  * •

$(X_{t})_{t\leq 0}$ has the law of
$(\widetilde{B}_{-2t}-(Q_{\gamma}-\alpha)t)_{t\leq 0}$, where $\widetilde{B}$
is a standard Brownian motion with $\widetilde{B}_{0}=0$.

  * •

$h_{\mathrm{L}}$, $(X_{t})_{t\leq 0}$ and $(X_{t})_{t\geq 0}$ are independent.

######  Remark 2.5.

Some care has to be taken when conditioning on a zero probability event. Fix
$a>0$ and let $(U_{t})_{t\geq 0}$ be $(B_{t}-at)_{t\geq 0}$ “conditioned to
stay negative”. By this we mean the weak limit as $\varepsilon\to 0$ of the
processes $(B_{t}-at)_{t\geq 0}$ conditioned to stay below $\varepsilon$. A
sample from this law can be drawn by sampling a standard Brownian motion
$\widehat{B}_{t}$, letting $\tau=\sup\\{t\geq 0:\widehat{B}_{t}-at\geq 0\\}$
(which is a.s. finite) and setting $U_{t}=\widehat{B}_{\tau+t}-a(\tau+t)$.

##  3 Natural measure

For any field $h$ we let $\nu_{h}$ denote the $2$-LQG boundary measure
associated with $h$, defined in (5). Moreover, we let $\eta$ be an
$\mathrm{SLE}_{4}$ in $\mathbb{H}$ from $0$ to $\infty$ and $(f_{t})$ its
centred Loewner chain. For $t\geq 0$ we denote by $\eta^{t}$ the curve
$\eta^{t}(u)=f_{t}(\eta(t+u))$ and note that $\eta^{0}=\eta$. Moreover, we
write $\psi_{t}=f_{t}^{-1}$ and let $f_{s,t}=f_{t}\circ\psi_{s}$ and
$\psi_{s,t}=f_{s,t}^{-1}=f_{s}\circ\psi_{t}$.

We let $h^{0}$ be a zero-boundary GFF independent of $\eta$ and for each $t>0$
let

$\displaystyle h^{t}=h^{0}\circ\psi_{t}+2\log|\psi_{t}^{\prime}|$ (6)

be the field on $\mathbb{H}$ formed by unzipping $h^{0}$ along $\eta^{0}$.
Then, we define the measure $\mu^{0}$ on $\eta^{0}$ by

$\displaystyle\mu^{0}|_{\eta^{0}([0,t])}(dz)=F(z)\mathbb{E}[\nu_{h^{t}}\,|\,\eta^{0}]\circ
f_{t}(dz),$ (7)

where $F(z)=r_{\mathbb{H}}(z)^{-1/2}$, and $r_{\mathbb{H}}(z)$ denotes the
conformal radius of $\mathbb{H}$ seen from $z$. An identity that we will use
several times is the following. If $\varphi$ be a conformal map, then

$\displaystyle\varphi^{\prime}(\varphi^{-1}(z))=\frac{1}{(\varphi^{-1})^{\prime}(z)}.$
(8)

We begin by proving that this definition of $\mu^{0}$ is consistent for
different values of $t$.

######  Lemma 3.1.

The definition of $\mu^{0}$ given in (7) is consistent for different values of
$t$. That is, if $0<s<t$, then for each $A\subset[0,s]$, we a.s. have that

$\displaystyle\int_{\eta^{0}(A)}F(z)\mathbb{E}[\nu_{h^{s}}\,|\,\eta^{0}]\circ
f_{s}(dz)=\int_{\eta^{0}(A)}F(z)\mathbb{E}[\nu_{h^{t}}\,|\,\eta^{0}]\circ
f_{t}(dz).$

###### Proof.

If $0<s<t$, then $h^{t}=h^{s}\circ\psi_{s,t}+2\log|\psi_{s,t}^{\prime}|$.
Thus,

$\displaystyle\nu_{h^{t}}\circ f_{t}(dz)$
$\displaystyle=\nu_{h^{s}\circ\psi_{s,t}+2\log|\psi_{s,t}^{\prime}|}\circ
f_{t}(dz)$ $\displaystyle=\left[\lim_{\varepsilon\to
0}\varepsilon\\!\left(\log(1/\varepsilon)-\frac{(h^{s}\circ\psi_{s,t})_{\varepsilon}+2\log|\psi_{s,t}^{\prime}|}{2}\right)e^{(h^{s}\circ\psi_{s,t})_{\varepsilon}+2\log|\psi_{s,t}^{\prime}|}\right]\circ
f_{s,t}\circ f_{s}(dz)$ $\displaystyle=\left[\lim_{\varepsilon\to
0}\varepsilon\\!\left(\log(1/\varepsilon)-\frac{h^{s}_{\varepsilon/|f_{s,t}^{\prime}|}-2\log|f_{s,t}^{\prime}|}{2}\right)e^{h^{s}_{\varepsilon/|f_{s,t}^{\prime}|}-2\log|f_{s,t}^{\prime}|}\right]\circ
f_{s}(dz)$ $\displaystyle=\left[\lim_{\varepsilon\to
0}\frac{\varepsilon}{|f_{s,t}^{\prime}|}\\!\left(\log(|f_{s,t}^{\prime}|/\varepsilon)-\frac{h^{s}_{\varepsilon/|f_{s,t}^{\prime}|}}{2}\right)e^{h^{s}_{\varepsilon/|f_{s,t}^{\prime}|}}\right]\circ
f_{s}(dz)$ $\displaystyle=\nu_{h^{s}}\circ f_{s}(dz),$

where in the third equality we used (8) and the fact that as $\varepsilon\to
0$, the preimages of circles of radius $\varepsilon$ around $f_{t}(z)$ under
$f_{s,t}$ are (roughly) circles of radius
$\varepsilon/|f_{s,t}^{\prime}(f_{s}(z))|$ around $f_{s}(z)$. This concludes
the proof. ∎

The rest of this section is divided into two subsections, the first of which
is focused on establishing that $\mu^{0}$ is locally finite as a measure on
$\mathbb{H}$, that is, for each compact $K\subset\mathbb{H}$, we have that
$\mu^{0}(K)<\infty$ a.s. The second subsection is devoted to proving the
conformal covariance of $\mu^{0}$ and then to deducing the local finiteness of
$\mu^{0}$ as a measure on $\eta$, that is, for each compact
$I\subset(0,\infty)$, we have that $\mu^{0}(\eta^{0}(I))<\infty$ a.s.

###  3.1 Local finiteness on $\mathbb{H}$

######  Lemma 3.2.

Almost surely, $\mu^{0}$ is locally finite as a measure on $\mathbb{H}$. That
is, $\mathbb{P}[\mu^{0}(K)<\infty]=1$ for each $K\subset\mathbb{H}$ compact.

We begin by noting that we can decompose a $(2,1)$-quantum wedge as the sum of
a zero-boundary GFF and a harmonic function. For the proof, we refer to [9]
(the parametrisation is slightly different but the proof is the same).

######  Lemma 3.3.

Let
$(\mathbb{H},h^{w},0,\infty)\sim\mathsf{QWedge}_{\bm{\gamma}=2}^{\bm{\alpha}=1}$
have the last exit parametrisation. Then, we can write
$h^{w}=h^{0}+\mathfrak{h}$, where $h^{0}$ is a zero-boundary GFF on
$\mathbb{H}$ and $\mathfrak{h}$ is a harmonic function on $\mathbb{H}$ which
is independent of $h^{0}$.

The following moment bound is the key ingredient in the proof of Lemma 3.2.
The reason for the choice of quantum surface is that
$\mathsf{QWedge}_{\bm{\gamma}=2}^{\bm{\alpha}=1}$ is natural in the context of
$\mathrm{SLE}_{4}$, as if we unzip such a surface along an $\mathrm{SLE}_{4}$
curve for a finite time, then the resulting law is still that of a
$\mathsf{QWedge}_{\bm{\gamma}=2}^{\bm{\alpha}=1}$, see [6, Theorem 1.5].

######  Lemma 3.4.

Let $\eta^{0}\sim\mathrm{SLE}_{4}$ and let
$(\mathbb{H},h^{w},0,\infty)\sim\mathsf{QWedge}_{\bm{\gamma}=2}^{\bm{\alpha}=1}$
have the last passage parametrisation and be independent of $\eta^{0}$. Set
$h^{w,t}=h^{w}\circ\psi_{t}+2\log|\psi_{t}^{\prime}|$. Then there exists
$p\in(0,1)$ such that for each $t\geq 0$,

$\displaystyle\mathbb{E}[\nu_{h^{w,t}}(f_{t}(\mathbb{D}\cap\mathbb{H}))^{p}]<\infty.$

Before proving Lemma 3.4, we begin by providing some moment bounds.

######  Lemma 3.5.

Let
$(\mathscr{S},h,-\infty,+\infty)\sim\mathsf{QWedge}_{\bm{\gamma}=2}^{\bm{\alpha}=1}$
have the last exit parametrisation and let for each $k\in\mathbb{Z}$,
$I_{k}=[k-1,k]\times\\{0,\pi\\}$. For each $p\in(0,1)$ there exists a constant
$C_{p}>0$ such that if $k\geq 1$, then $\mathbb{E}[\nu_{h}(I_{k})^{p}]\leq
C_{p}$ and if $k\leq 0$, then

$\displaystyle\mathbb{E}[\nu_{h}(I_{k})^{p}]\leq C_{p}e^{-(4p^{2}+2p)k}.$

###### Proof.

We let $h=X+h_{\mathrm{L}}$ be the decomposition into the average on vertical
lines process $X$ and the lateral part $h_{\mathrm{L}}$ of $h$. By [8, Lemma
A.4] we have that $\mathbb{E}[\nu_{h_{\mathrm{L}}}(I_{k})^{p}]<\infty$ for all
$k\in\mathbb{Z}$ and $p\in(0,1)$. Moreover, we have that

$\displaystyle\nu_{h}(I_{k})\leq\nu_{h_{\mathrm{L}}}(I_{k})\exp\\!\Big{(}2\sup_{t\in[k-1,k]}X_{t}\Big{)}.$
(9)

Since $X_{t}$ is non-positive whenever $t\geq 0$, the first assertion follows.
Consider now the case $k\leq 0$, so that the Brownian motion in the process
$X$ is not conditioned on any event. Then,

$\displaystyle\sup_{t\in[k-1,k]}X_{t}\leq
1-k+\sup_{t\in[k-1,k]}\widetilde{B}_{2t}=1-k+\widetilde{B}_{-2k}+\sup_{t\in[k-1,k]}\widetilde{B}_{-2t}-\widetilde{B}_{-2k}.$

Thus, since $\widetilde{B}$ has stationary and independent increments and for
a Brownian motion $\widehat{B}$ and any $c>0$, the expectation
$\mathbb{E}[\exp(c\sup_{t\in[0,2]}\widehat{B}_{t})]$ is finite, it follows
from (9) that for $p\in(0,1)$,

$\displaystyle\mathbb{E}[\nu_{h}(I_{k})^{p}]$
$\displaystyle\leq\mathbb{E}[\nu_{h_{\mathrm{L}}}(I_{k})^{p}]\mathbb{E}\\!\left[\exp\\!\left(2p\sup_{t\in[k-1,k]}X_{t}\right)\right]$
$\displaystyle=e^{2p(1-k)}\mathbb{E}[\nu_{h_{\mathrm{L}}}(I_{k})^{p}]\mathbb{E}[\exp(2pB_{-2k})]\mathbb{E}\\!\left[\exp\\!\left(2p\sup_{t\in[0,2]}\widehat{B}_{t}\right)\right]$
$\displaystyle\leq C_{p}e^{-(4p^{2}+2p)k}$

where $C_{p}$ is some positive constant depending only on $p$. ∎

###### Proof of Lemma 3.4.

Let $\tau=\sup\\{t\geq 0:\eta^{0}(t)\in\mathbb{D}\\}$. We note that by
conformal invariance,

$\displaystyle\nu_{h^{w,s}}(f_{s}(\mathbb{D}\cap\mathbb{H}))\leq\nu_{h^{w,\tau}}(f_{\tau}(\mathbb{D}\cap\mathbb{H}))=\nu_{h^{w,t}}(f_{t}((\mathbb{D}\cap\mathbb{H}))$

whenever $s\leq\tau\leq t$. By [21, Theorem 4.1] we have that

$\displaystyle\mathbb{P}\\!\left[\sup_{0\leq t\leq\tau}|\eta^{0}(t)|\geq
R\right]\lesssim R^{-2}.$ (10)

We let $\tau_{R}=\inf\\{t\geq 0:|\eta^{0}(t)|\geq R\\}$ and note that for all
$0\leq t\leq\tau_{R}$, $|f_{t}(0^{-})|,|f_{t}(0^{+})|\leq 4R$. Indeed, this
follows immediately from [18, Equation (8)] and a comparison with the compact
$\mathbb{H}$-hull $R\overline{\mathbb{D}}\cap\mathbb{H}$. We shall now bound
moments of the quantum length of $[-4R,4R]$.

We first bound $p$th moment of the quantum length of $[-4R,-1]\cup[1,4R]$. As
above, let $I_{k}=[k-1,k]\times\\{0,\pi\\}$. Then, letting
$(\mathscr{S},h^{S},-\infty,+\infty)\sim\mathsf{QWedge}_{\bm{\gamma}=2}^{\bm{\alpha}=1}$,
this corresponds to bounding $\mathbb{E}[\nu_{h^{S}}([-\log
4R,0]\times\\{0,\pi\\})^{p}]$. By Lemma 3.5 and the inequality
$(\sum_{j}x_{j})^{p}\leq\sum_{j}x_{j}^{p}$ (for $x_{j}>0$, $0<p<1$),

$\displaystyle\mathbb{E}[\nu_{h^{S}}([-\log 4R,0]\times\\{0,\pi\\})^{p}]$
$\displaystyle\leq\sum_{k=0}^{\lceil\log
4R\rceil}\mathbb{E}[\nu_{h^{S}}(I_{-k})^{p}]\leq C_{p}\sum_{k=0}^{\lceil\log
4R\rceil}e^{(4p^{2}+2p)k}$ $\displaystyle\lesssim\int_{0}^{\lceil\log
4R\rceil}e^{(4p^{2}+2p)x}dx\lesssim R^{4p^{2}+2p},$

where the implicit constants depend on $p$. Moreover, let as in Remark 2.5,
$\widehat{B}$ be a standard Brownian motion, $\tau=\sup\\{t\geq
0:\widehat{B}_{t}-t\\}$ and such that $X_{t}=\widehat{B}_{\tau+t}-(\tau+t)$,
and let $M=\sup_{t\geq 0}\widehat{B}_{t}-t$. Then, letting
$X_{k}^{*}=\sup_{t\in[k-1,k]}X_{t}$ and
$k^{*}=\arg\max_{t\in[k-1,k]}\widehat{B}_{t}-t$, we have that

$\displaystyle\mathbb{E}[\nu_{h^{S}}([0,\infty)\times\\{0,\pi\\})^{p}]$
$\displaystyle\leq\mathbb{E}\\!\left[\sum_{k=1}^{\infty}\exp\\!\left(2pX_{k}^{*}\right)\nu_{h_{\mathrm{L}}}(I_{k})^{p}\right]\lesssim\mathbb{E}\\!\left[\sum_{k=1}^{\infty}\exp\\!\left(2pX_{k}^{*}\right)\right]$
$\displaystyle\leq\mathbb{E}\\!\left[\sum_{k=1}^{\infty}\exp\\!\left(2p(\widehat{B}_{k^{*}}-k^{*})\right)\right]=\mathbb{E}\\!\left[\mathbb{E}\\!\left[\sum_{k=1}^{\infty}\exp\\!\left(2p(\widehat{B}_{k^{*}}-k^{*})\right)\middle|M\right]\right]$
$\displaystyle\lesssim\mathbb{E}[\exp(2pM)]\quad(\cite[cite]{[\@@bibref{}{dms2021mating}{}{},
{Lemma}\leavevmode\nobreak\ {A}.5]})$

Letting $T_{x}=\inf\\{t\geq 0:\widehat{B}_{t}\geq x\\}$, we have that
$\mathbb{P}(M>x)=\mathbb{P}(T_{x}<\infty)=\exp(-2x)$ and hence, since
$p\in(0,1)$, $\mathbb{E}[\exp(2pM)]$ is finite. Consequently,

$\displaystyle\mathbb{E}[\nu_{h^{S}}([-\log
4R,\infty]\times\\{0,\pi\\})^{p}]\lesssim R^{4p^{2}+2p}$

where the implicit depends only on $p$. We let $E_{n}$ be the event that
$\sup_{0\leq t\leq\tau}|\eta(t)|\in(n-1,n]$. Then, by [6, Theorem 1.5], we
have that

$\displaystyle\mathbb{E}[\nu_{h^{w,\tau}}(f_{\tau}(\mathbb{D}\cap\mathbb{H}))^{p}]$
$\displaystyle=\sum_{n=0}^{\infty}\mathbb{E}[\nu_{h^{w,\tau}}(f_{\tau}(\mathbb{D}\cap\mathbb{H}))^{p}\,|\,E_{n}]\mathbb{P}(E_{n})$
$\displaystyle\leq\sum_{n=0}^{\infty}\mathbb{E}[\nu_{h^{w}}([-4n,4n])^{p}]\mathbb{P}(E_{n})$
$\displaystyle\lesssim\sum_{n=1}^{\infty}n^{4p^{2}+2p}n^{-2}$

which is finite if we pick $p$ small enough, so that $4p^{2}+2p-2<-1$. ∎

###### Proof of Lemma 3.2.

Let $p\in(0,1)$ be as in Lemma 3.4. We shall begin by showing that
$\mathbb{E}[\nu_{h^{t}}(f_{t}(K))^{p}]\newline <\infty$ for each
$K\subset\tfrac{1}{2}\overline{\mathbb{D}}\cap\mathbb{H}$ compact and each
$t>0$.

Fix some compact $K\subset\tfrac{1}{2}\overline{\mathbb{D}}\cap\mathbb{H}$ and
let $\delta=\mathrm{dist}(K,\partial\mathbb{H})>0$. We decompose
$h^{w}=h^{0}+\mathfrak{h}$ as in Lemma 3.3 and note that since $\delta>0$, we
have that $\mathfrak{h}$ is almost surely bounded on $K$. Thus, if $E_{K}$
denotes the event that $\sup_{z\in K}|\mathfrak{h}(z)|\leq C$, then
$\mathbb{P}[E_{K}]\to 1$ as $C\to\infty$. We choose $C>0$ large enough so that
$\mathbb{P}[E_{K}]\geq 1/2$. Then, it follows that

$\displaystyle\mathbb{E}[\nu_{h^{t}}(f_{t}(K))^{p}\,|\,\mathfrak{h}]\mathbf{1}_{E_{K}}\leq
e^{Cp}\mathbb{E}[\nu_{h^{w,t}}(f_{t}(K))^{p}\,|\,\mathfrak{h}]\mathbf{1}_{E_{K}}\leq
e^{Cp}\mathbb{E}[\nu_{h^{w,t}}(f_{t}(K))^{p}\,|\,\mathfrak{h}].$ (11)

Since
$\mathbb{E}[\mathbb{E}[\nu_{h^{w,t}}(f_{t}(K))^{p}\,|\,\mathfrak{h}]]=\mathbb{E}[\nu_{h^{w,t}}(f_{t}(K))^{p}]<\infty$,
it follows that $\mathbb{E}[\nu_{h^{w,t}}(f_{t}(K))^{p}\,|\,\mathfrak{h}]$ is
almost surely finite. By the independence of $h^{0}$ and $\mathfrak{h}$, we
have that
$\mathbb{E}[\nu_{h^{t}}(f_{t}(K))^{p}\,|\,\mathfrak{h}]=\mathbb{E}[\nu_{h^{t}}(f_{t}(K))^{p}]$.
Since the right-hand side of (11) is a.s. finite it follows that
$\mathbb{E}[\nu_{h^{t}}(f_{t}(K))^{p}]<\infty$.

Next, we shall show that $\mu^{0}(K)<\infty$ almost surely. Let $\tau$ be the
last exit time of $\mathbb{D}$ for $\eta^{0}$. Since $\eta^{0}$ is transient,
we have that $\tau<\infty$ almost surely and hence that if $E_{T}^{*}$ is the
event that $\tau\leq T$, then $\mathbb{P}[E_{T}^{*}]\to 1$ as $T\to\infty$.
Thus, since $\mathrm{dist}(z,\mathbb{H})\geq\delta$ for all $z\in K$, we have
that

$\displaystyle\mathbb{E}[\mu^{0}(K)^{p}\mathbf{1}_{E_{T}^{*}}]\leq\delta^{-p/2}\mathbb{E}[\nu_{h^{\tau}}(f_{\tau}(K))^{p}\mathbf{1}_{E_{T}^{*}}]\leq\delta^{-p/2}\mathbb{E}[\nu_{h^{T}}(f_{T}(K))^{p}]<\infty.$
(12)

Assume for the sake of contradiction that
$\mathbb{P}[\mu^{0}(K)=\infty]=p_{0}>0$. Choose $T>0$ large enough so that
$\mathbb{P}[E_{T}^{*}]\geq 1-p_{0}/2$. Then, it follows from (12) that
conditional on the event $E_{T}^{*}$, $\mu^{0}(K)$ is a.s. finite, and
consequently, $\\{\mu^{0}(K)=\infty\\}$ is contained in the union of
$(E_{T}^{*})^{c}$ and a zero probability event. This, however, is a
contradiction since $\mathbb{P}[(E_{T}^{*})^{c}]\leq p_{0}/2$. Hence
$\mu^{0}(K)$ is a.s. finite.

We now consider a general compact $\widetilde{K}\subset\mathbb{H}$ and let
$R=\inf\\{r>0\colon\widetilde{K}\subset B(0,r/2)\\}$ and
$\delta=\mathrm{dist}(\widetilde{K},\partial\mathbb{H})>0$. Let
$\varphi_{R}(z)=z/R$ and note that
$K\coloneqq\varphi_{R}(\widetilde{K})\subset\tfrac{1}{2}\overline{\mathbb{D}}\cap\mathbb{H}$.
Moreover, we note that $\varphi_{R}(\eta^{0})\sim\mathrm{SLE}_{4}$,
$\widetilde{h}^{0}\coloneqq h^{0}\circ\varphi_{R}^{-1}$ is a zero-boundary GFF
on $\mathbb{H}$. Furthermore, we let $\sigma$ be the last exit time of
$B(0,R)$ for $\eta^{0}$ and $(\widetilde{f}_{t})$ be the Loewner chain
corresponding to the curve
$\widetilde{\eta}^{0}(t)\coloneqq\varphi_{R}(\eta^{0}(t))$, that is,
$\widetilde{f}_{t}(z)=\tfrac{1}{R}f_{t}(Rz)$, and we let
$\widetilde{\psi}_{t}(z)=\widetilde{f}_{t}^{-1}(z)=\tfrac{1}{R}\psi_{t}(Rz)$
and
$\widetilde{h}^{t}=\widetilde{h}^{0}\circ\widetilde{\psi}_{t}+2\log|\widetilde{\psi}_{t}^{\prime}|$.
Then by the LQG coordinate change and the scale invariance of $\eta^{0}$ and
$h^{0}$, it follows that a.s.

$\displaystyle\nu_{h^{\sigma}}(f_{\sigma}(\widetilde{K}))=\nu_{\widetilde{h}^{\sigma}+2\log
R}(\widetilde{f}_{\sigma}(K))\overset{d}{=}\nu_{h^{\tau}+2\log
R}(f_{\tau}(K))=R^{2}\nu_{h^{\tau}}(f_{\tau}(K)).$

Thus, it follows analogously to the above that
$\mathbb{E}[\nu_{h^{T}}(f_{T}(\widetilde{K}))^{p}]$ is almost surely finite
for $T>0$ and hence that $\mu^{0}(\widetilde{K})$ is as well. ∎

###  3.2 Conformal covariance

Fix $s>0$ and let $\widetilde{h}^{s}$ be a zero-boundary GFF on $\mathbb{H}$,
independent of $\eta^{0}$. This then gives us a field
$\widetilde{h}^{0}=\widetilde{h}^{s}\circ f_{s}+2\log|f_{s}^{\prime}|$ by
zipping up along $\eta^{0}$, and hence a family of fields
$(\widetilde{h}^{t})_{t\geq 0}$ by letting
$\widetilde{h}^{t}=\widetilde{h}^{0}\circ\psi_{t}+2\log|\psi_{t}^{\prime}|$.
We recall that
$f_{s,t}=f_{t}\circ\psi_{s}\colon\mathbb{H}\setminus\eta^{s}([0,t-s])\to\mathbb{H}$
and define the measure $\widetilde{\mu}^{s}$ by

$\displaystyle\widetilde{\mu}^{s}|_{\eta^{s}([0,t-s])}(dz)=F(z)\mathbb{E}[\nu_{\widetilde{h}^{t}}\,|\,\eta^{s}]\circ
f_{s,t}(dz).$ (13)

Recall from (3) that
$\mu^{t}(dz)=|\psi_{t}^{\prime}(z)|^{-d_{4}}(\mu^{0}\circ\psi_{t})(dz)$, where
$d_{4}=3/2$.

######  Lemma 3.6.

Almost surely, $\widetilde{\mu}^{s}=\mu^{s}$, that is,

$\displaystyle\mu^{0}|_{\eta^{0}([s,\infty))}\circ\psi_{s}(dz)=|\psi_{s}^{\prime}(z)|^{3/2}\widetilde{\mu}^{s}(dz).$

###### Proof.

Since $\widetilde{h}^{s}$ is a zero-boundary GFF in $\mathbb{H}$, we have that
$\widetilde{h}^{s}\circ f_{s}$ is a zero-boundary GFF in
$\mathbb{H}\setminus\eta^{0}([0,s])$. Thus we may assume that
$\widetilde{h}^{s}$ and $h^{0}$ are coupled together in such a way that we can
define a Gaussian field $\mathfrak{H}$, which is conditionally independent of
$\widetilde{h}^{s}$ given $\eta^{0}$ and such that
$h^{0}=\widetilde{h}^{s}\circ f_{s}+\mathfrak{H}$. Then the covariance kernel
of $\mathfrak{H}$ is given by

$\displaystyle
G_{\mathbb{H}}(z,w)-G_{\mathbb{H}\setminus\eta^{0}([0,s])}(z,w)=G_{\mathbb{H}}(z,w)-G_{\mathbb{H}}(f_{s}(z),f_{s}(w))$

and hence the variance of $\mathfrak{H}$ at a point $z$ is well-defined and
equal to

$\displaystyle\mathrm{Var}\,\mathfrak{H}(z)=\lim_{\varepsilon\to
0}\mathrm{Var}\,\mathfrak{H}_{\varepsilon}(z)=\log r_{\mathbb{H}}(z)-\log
r_{\mathbb{H}}(f_{s}(z))+\log|f_{s}^{\prime}(z)|$

(here $\mathfrak{H}_{\varepsilon}(z)$ denotes the average value of
$\mathfrak{H}$ on the circle $\partial B(z,\varepsilon)$). The term
$\log|f_{s}^{\prime}(z)|$ comes from the change of variables dilating the ball
of radius $\varepsilon$ roughly by a factor of $|f_{s}^{\prime}(z)|$.

We note that
$h^{t}=h^{0}\circ\psi_{t}+2\log|\psi_{t}^{\prime}|=\widetilde{h}^{t}+\mathfrak{H}\circ\psi_{t}+2\log|\psi_{s}^{\prime}|\circ\psi_{s,t}$
and that since $\mathfrak{H}$ is centred and $\mathrm{Var}\,\mathfrak{H}(z)$
is finite, it follows from [16, Lemma 2.1] that

$\displaystyle\mathbb{E}\\!\left[\lim_{\varepsilon\to
0}\varepsilon\\!\left(\frac{(\mathfrak{H}\circ\psi_{t})_{\varepsilon}}{2}+\log|\psi_{s}^{\prime}|\circ\psi_{s,t}\right)e^{\widetilde{h}^{t}_{\varepsilon}+(\mathfrak{H}\circ\psi_{t})_{\varepsilon}+2\log|\psi_{s}^{\prime}|\circ\psi_{s,t}}\,\middle|\,\eta^{0}\right]\circ
f_{t}(dz)$

is the zero measure. It follows that

$\displaystyle\mu^{0}|_{\eta^{0}([0,t])}(dz)=$
$\displaystyle=F(z)\mathbb{E}\\!\left[\lim_{\varepsilon\to
0}\varepsilon\\!\left(\log\\!\left(\frac{1}{\varepsilon}\right)-\frac{\widetilde{h}^{t}_{\varepsilon}+(\mathfrak{H}\circ\psi_{t})_{\varepsilon}+2\log|\psi_{s}^{\prime}|\circ\psi_{s,t}}{2}\right)e^{\widetilde{h}^{t}_{\varepsilon}+(\mathfrak{H}\circ\psi_{t})_{\varepsilon}+2\log|\psi_{s}^{\prime}|\circ\psi_{s,t}}\,\middle|\,\eta^{0}\right]\circ
f_{t}(dz)$ $\displaystyle=F(z)\mathbb{E}\\!\left[\lim_{\varepsilon\to
0}\varepsilon\\!\left(\log\left(\frac{1}{\varepsilon}\right)-\frac{\widetilde{h}^{t}_{\varepsilon}}{2}\right)|\psi_{s}^{\prime}|^{2}\circ\psi_{s,t}e^{\widetilde{h}^{t}_{\varepsilon}+(\mathfrak{H}\circ\psi_{t})_{\varepsilon}}\,\middle|\,\eta^{0}\right]\circ
f_{t}(dz)$
$\displaystyle=F(z)|f_{s}(z)|^{-2}\mathbb{E}[e^{\mathfrak{H}(z)}\,|\,\eta^{0}]\mathbb{E}\\!\left[\lim_{\varepsilon\to
0}\varepsilon\\!\left(\log\left(\frac{1}{\varepsilon}\right)-\frac{\widetilde{h}^{t}_{\varepsilon}}{2}\right)e^{\widetilde{h}^{t}_{\varepsilon}}\,\middle|\,\eta^{0}\right]\circ
f_{t}(dz),$

where (8) was used in the last inequality. Since the conditional law of
$\mathfrak{H}(z)$ given $\eta^{0}$ is that of a centred Gaussian, we have that

$\displaystyle\mathbb{E}[e^{\mathfrak{H}(z)}\,|\,\eta^{0}]=r_{\mathbb{H}}(z)^{1/2}r_{\mathbb{H}}(f_{s}(z))^{-1/2}|f_{s}^{\prime}(z)|^{1/2}=\frac{F(f_{s}(z))}{F(z)}|f_{s}^{\prime}(z)|^{1/2}$

and hence

$\displaystyle\mu^{0}|_{\eta^{0}([0,t])}(dz)=F(f_{s}(z))|f_{s}^{\prime}(z)|^{-3/2}\mathbb{E}\\!\left[\lim_{\varepsilon\to
0}\varepsilon(\log(1/\varepsilon)-\widetilde{h}^{t}_{\varepsilon}/2)e^{\widetilde{h}^{t}_{\varepsilon}}\,\middle|\,\eta^{0}\right]\circ
f_{t}(dz).$

Consequently,

$\displaystyle\mu^{0}|_{\eta^{0}([s,t])}\circ\psi_{s}(dz)$
$\displaystyle=F(z)|f_{s}^{\prime}(\psi_{s}(z))|^{-3/2}\mathbb{E}\\!\left[\lim_{\varepsilon\to
0}\varepsilon(\log(1/\varepsilon)-\widetilde{h}^{t}_{\varepsilon}/2)e^{\widetilde{h}^{t}_{\varepsilon}}\,\middle|\,\eta^{0}\right]\circ
f_{s,t}(dz)$
$\displaystyle=|\psi_{s}^{\prime}(z)|^{3/2}F(z)\mathbb{E}[\nu_{\widetilde{h}^{t}}\,|\,\eta^{s}]\circ
f_{s,t}(dz)$
$\displaystyle=|\psi_{s}^{\prime}(z)|^{3/2}\widetilde{\mu}^{s}|_{\eta^{s}([0,t-s])}(dz),$

where (8) was used in the second equality. Thus, the proof is complete. ∎

The following lemma is proved in the same way as Lemma 3.6, and hence the
proof is omitted.

######  Lemma 3.7.

Let $\phi_{a}(z)=az$ for $a>0$. Then,

$\displaystyle\mathbb{E}[\mu^{0}]\circ\phi_{a}(dz)=a^{3/2}\mathbb{E}[\mu^{0}](dz).$

We need that the intensity is absolutely continuous with respect to two-
dimensional Lebesgue measure. In essence, that the randomness of the curve
causes an averaging of the measure $\mathbb{E}[\mu^{0}]$, so that its mass is
spread out over the entire $\mathbb{H}$, rather than in a subset of zero
Lebesgue measure. The following was proved for the measures on
$\mathrm{SLE}_{\kappa}$ for $\kappa\in(4,8)$, see [15, Lemma 3.6], but the
exact same proof works with the measure $\mu^{0}$ on $\mathrm{SLE}_{4}$.

######  Lemma 3.8.

The measure $\mathbb{E}[\mu^{0}]$ is absolutely continuous with respect to
Lebesgue measure.

Next, we recall the following lemma of [15].

######  Lemma 3.9 (Lemma 3.7 of [15]).

For each $a>0$, let $\phi_{a}(z)=az$. Let $m$ be a measure on $\mathbb{H}$
which is absolutely continuous with respect to Lebesgue measure and satisfies

$\displaystyle m\circ\phi_{a}(dz)=a^{d}m(dz)$

for some $d>1$ and all $a>0$. Then there exists some function $H(z)=H(\arg z)$
such that

$\displaystyle m(dz)=H(\arg z)\mathrm{Im}(z)^{d-2}dz.$

By Lemmas 3.7 and 3.8 the conditions of Lemma 3.9 are satisfied for
$\mathbb{E}[\mu^{0}]$. Next, we note the form of $H$ in the case of
$m=\mathbb{E}[\mu^{0}]$.

######  Lemma 3.10.

There is some constant $c>0$ such that

$\displaystyle\mathbb{E}[\mu^{0}](dz)=c\sin(\arg z)\mathrm{Im}(z)^{-1/2}dz.$

###### Proof.

This is proved exactly in the same way as [15, Lemma 3.8]. ∎

We wrap up this section by deducing the following. The proof is the same as
that of [15, Lemma 3.9], but it is very short so we repeat it here.

######  Lemma 3.11.

Almost surely, $\mu^{0}$ is locally finite. That is, almost surely,

$\displaystyle\mu^{0}(\eta([s,t]))<\infty\quad\text{for all}\quad 0<s<t.$

###### Proof.

Note that by Lemma 3.10, $\mathbb{E}[\mu^{0}(B(0,R))]<\infty$ for each $R>0$,
so that a.s., $\mu^{0}(B(0,R))$ is finite. Moreover, for each $0\leq s\leq t$,
we have that $\mathbb{P}(\eta([s,t])\subset B(0,R))\to 1$ as $R\to\infty$.
Finally, since $\mu^{0}(\eta([s,t]))\leq\mu^{0}(B(0,R))$ on the event
$\\{\eta([s,t])\subset B(0,R)\\}$, it follows that for any $0\leq s\leq t$,
$\mu([s,t])$ is a.s. finite. ∎

###### Proof of Theorem 1.1.

By Lemmas 3.6 and 3.11 and Theorem 2.1 the conclusion of the theorem holds. ∎

## References

  * [1] V. Beffara.  The dimension of the SLE curves.  Ann. Probab., 36(4):1421–1452, 2008.
  * [2] S. Benoist.  Natural parametrization of SLE: the Gaussian free field point of view.  Electron. J. Probab., 23:Paper No. 103, 16, 2018.
  * [3] G. Cai and X. Li.  On Natural Measures of SLE- and CLE-Related Random Fractals.  arXiv e-prints, page arXiv:2205.01584, May 2022.  To appear in Ann. Inst. Henri Poincaré Probab. Stat.
  * [4] B. Duplantier, J. Miller, and S. Sheffield.  Liouville quantum gravity as a mating of trees.  Astérisque, (427):viii+257, 2021.
  * [5] N. Holden, X. Li, and X. Sun.  Natural parametrization of percolation interface and pivotal points.  Ann. Inst. Henri Poincaré Probab. Stat., 58(1):7–25, 2022.
  * [6] N. Holden and E. Powell.  Conformal welding for critical Liouville quantum gravity.  Ann. Inst. Henri Poincaré Probab. Stat., 57(3):1229–1254, 2021\.
  * [7] O. Kallenberg.  Random measures, theory and applications, volume 77 of Probability Theory and Stochastic Modelling.  Springer, Cham, 2017.
  * [8] K. Kavvadias, J. Miller, and L. Schoug.  Regularity of the $\mathrm{SLE}_{4}$ uniformizing map and the $\mathrm{SLE}_{8}$ trace.  arXiv e-prints, page arXiv:2107.03365, July 2021.
  * [9] K. Kavvadias, J. Miller, and L. Schoug.  Conformal removability of non-simple Schramm-Loewner evolutions.  arXiv e-prints, page arXiv:2302.10857, Feb. 2023.
  * [10] G. F. Lawler and M. A. Rezaei.  Minkowski content and natural parameterization for the Schramm-Loewner evolution.  Ann. Probab., 43(3):1082–1120, 2015.
  * [11] G. F. Lawler, O. Schramm, and W. Werner.  Conformal invariance of planar loop-erased random walks and uniform spanning trees.  Ann. Probab., 32(1B):939–995, 2004.
  * [12] G. F. Lawler and S. Sheffield.  A natural parametrization for the Schramm-Loewner evolution.  Ann. Probab., 39(5):1896–1937, 2011.
  * [13] G. F. Lawler and F. Viklund.  Convergence of loop-erased random walk in the natural parameterization.  Duke Math. J., 170(10):2289–2370, 2021.
  * [14] G. F. Lawler and W. Zhou.  SLE curves and natural parametrization.  Ann. Probab., 41(3A):1556–1584, 2013.
  * [15] J. Miller and L. Schoug.  Existence and uniqueness of the conformally covariant volume measure on conformal loop ensembles.  arXiv e-prints, page arXiv:2201.01748, Jan. 2022.  To appear in Ann. Inst. Henri Poincaré Probab. Stat.
  * [16] E. Powell.  Critical Gaussian multiplicative chaos: a review.  Markov Process. Related Fields, 27(4):557–506, 2021.
  * [17] S. Rohde and O. Schramm.  Basic properties of SLE.  Ann. of Math. (2), 161(2):883–924, 2005.
  * [18] L. Schoug.  A multifractal boundary spectrum for ${\rm SLE}_{\kappa}(\rho)$.  Probab. Theory Related Fields, 178(1-2):173–233, 2020.
  * [19] L. Schoug, A. Sepúlveda, and F. Viklund.  Dimensions of Two-Valued Sets via Imaginary Chaos.  International Mathematics Research Notices, 10 2020.  rnaa250.
  * [20] O. Schramm.  Scaling limits of loop-erased random walks and uniform spanning trees.  Israel J. Math., 118:221–288, 2000.
  * [21] H. Wu and D. Zhan.  Boundary arm exponents for SLE.  Electron. J. Probab., 22:Paper No. 89, 26, 2017.