Reasoning about the Garden of Forking Paths

Yao Li

University of Pennsylvania
3330 Walnut St

Li-yao Xia

University of Pennsylvania
3330 Walnut St

Stephanie Weirich

University of Pennsylvania
3330 Walnut St

Lazy evaluation is a powerful tool for functional programmers. It enables the
concise expression of on-demand computation and a form of compositionality not
available under other evaluation strategies. However, the stateful nature of
lazy evaluation makes it hard to analyze a program's computational cost,
either informally or formally. In this work, we present a novel and simple
framework for formally reasoning about lazy computation costs based on a
recent model of lazy evaluation: clairvoyant call-by-value. The key feature of
our framework is its simplicity, as expressed by our definition of
the clairvoyance monad. This monad is both simple to define (around 20
lines of Coq) and simple to reason about. We show that this monad can be
effectively used to mechanically reason about the computational cost of lazy
functional programs written in Coq.

<concept_desc>Software and its engineering Functional languages</concept_desc>
<concept_desc>Theory of computation Denotational semantics</concept_desc>
<concept_desc>Theory of computation Program specifications</concept_desc>
<concept_desc>Theory of computation Program verification</concept_desc>
<concept_desc>Software and its engineering Software performance</concept_desc>

[500]Software and its engineering Functional languages
[500]Theory of computation Denotational semantics
[500]Theory of computation Program specifications
[500]Theory of computation Program verification
[500]Software and its engineering Software performance

§ INTRODUCTION

Lazy evaluation <cit.>, or the call-by-need calling convention, is
a distinguishing feature in some functional programming languages—Haskell
being the most notable example.
Rather than evaluating eagerly, a lazy evaluator stores computations in a
thunk and only evaluates the thunk when the data is needed. This feature
avoids unneeded computation and enables better
modularity in functional programming <cit.>.
However, with convenience in expressiveness comes challenge in
reasoning—especially so for cost analysis—because it's far less
obvious if, when, and how much a computation is evaluated.
We believe proof assistants can help to reason formally about semantics so
intricate and subtle.

However, modeling laziness formally is difficult.
The semantics for call-by-need evaluation is more complex than that of
call-by-name or call-by-value, which can be described merely through
substitution. Traditional presentations <cit.> of
call-by-need semantics are fundamentally stateful, based on heaps that
contain thunks which must be updated during evaluation.

Rather than directly dealing with such complexity, we take advantage of a new
way of modeling call-by-need: clairvoyant
call-by-value <cit.>. The key observation of this new model is
that although whether a term gets evaluated matters, it doesn't
matter when in run-time cost analysis. Therefore, instead of storing the
computations in a thunk, the clairvoyant call-by-value model makes use of
nondeterminism to evaluate the data in one branch and skip evaluation in
another. Eventually, one successful branch of evaluation will faithfully model
the result and cost of the call-by-need evaluation.

Based on clairvoyant evaluation, we propose a novel framework for reasoning
about laziness using the Coq proof assistant, a dependently-typed interactive
theorem prover <cit.>. Our framework is based on an annotated model similar
to that of <cit.> and of <cit.>, but our work does not
require an explicit notion of laziness to reason about computation costs under
lazy evaluation.

We make the following contributions:

* We present the clairvoyance monad, a model of laziness that can be
shallowly embedded in Coq by distilling two core features of clairvoyant
evaluation: nondeterminism and cost accumulation. One key feature of the
clairvoyance monad is its simplicity: it consists of only a handful of basic
combinators and can be defined with around 20 lines of code in
Coq (<Ref>).

* We develop a translation from a lazy calculus to programs in this
monad that captures the semantics of clairvoyant call-by-value evaluation.
Compared with the denotational semantics of <cit.>, our
translation deals with typed programs, does not rely on domain
theory, and accounts for the cost of every nondeterministic
execution (<Ref>).

* One challenge arising from clairvoyant evaluation is to reason about
nondeterminism. We develop dual logics of over-
and under-approximations similar to those
of <cit.> to reason about lazy
programs. We show that formal reasoning of computation cost based on these
logics can be done in a local and modular
way (<Ref>).

* We demonstrate the usefulness of our technique via case studies of tail
recursion that capture the unique characteristics of lazy
evaluation (<Ref>).

Our paper ends with a comparison of related research in <ref> and a
discussion of future work in <ref>.
In the next section, below, we introduce our approach at a high level and present our running example.

§ MOTIVATING EXAMPLE

We start by providing an informal overview of our approach on a small example
that exhibits laziness. Consider the following program, written in Gallina, the
functional programming language of the Coq proof assistant <cit.>:

Gallina can be compiled to use lazy evaluation via extraction to Haskell. The
functions append and take in this example are equivalent to their
Haskell counterparts, and their definitions are shown
in <ref>. [For reasons that we will explain
in <ref>, these functions are written in A-Normal
Form <cit.>, but that doesn't matter so much here.]  These examples use
Gallina's inductively defined lists, which are a subset of Haskell's list type.
Although working with infinite data types is another useful application of lazy
evaluation, many algorithms manipulate only finite data
structures <cit.>. Hence, we believe inductive lists are
representative of how lists are used in practice even in Haskell.

The pure functional definitions of append and take.

To estimate the time it takes to evaluate a program, its cost, we can start by
counting the number of steps in some operational semantics, or some
proportional quantity. Let us count function calls informally.

Lazy evaluation leads us immediately to an impasse, because it is not even clear
what it means to “run” a lazy program. Lazy programs are demand-driven, so we
have to specify some model of “demand”. A common working model is that lazy
programs will be forced during the evaluation of a whole program, but it is
not so practical to reason about the behaviors of arbitrary programs.  A more useful
approach is to start from a more familiar place: call-by-value. Indeed, programs
under the call-by-value evaluation strategy have a relatively straightforward
cost model. Laziness adds a twist to it: we might not need all of the result,
in which case we allow ourselves to skip some computations.

With that new ability, we face the problem of
deciding which computations to skip. This decision inherently
depends on how much of the overall result will be needed.
For concreteness, let us require all of our example list
take n (append xs ys) to be evaluated.
We start by evaluating append xs ys, unfolding the
program in call-by-value. There are two cases to consider: the length of
xs may be less than n, in which case we will fully evaluate
append xs ys in length xs + 1 calls—where the final nil
takes one call. Or length xs may be greater than or equal to n,
then we can stop after n calls, leaving the result of the next call
“undefined”. Either way, we will produce some partially defined list zs
after at most n calls. We then let take n zs run to the end in at
most n + 1 calls, thus producing all elements of take n (append xs
ys), as we demanded initially.  In total, that took at most 2 * n + 1
calls. In particular, that cost is independent of the length of xs or
That exemplifies one of the core motivations of laziness: you only pay for what
you need.

That idea of “call-by-value with a twist” is made formal by the concept of
clairvoyant evaluation <cit.>.

§.§ Clairvoyant Evaluation

The key to formalize the reasoning above is to view lazy programs
as nondeterministic programs. Clairvoyant evaluation works in a way
similar to nondeterministic automata, which choose one of multiple successor
states by “guessing” the path to success. In our earlier reasoning, we
evaluated append xs ys in call-by-value until we decided to stop at a
point. When to stop was not decided by the state of the program, but by a
“guess” based on the clairvoyant knowledge that we would only need n
elements in the end. This intuition allows us to define a general semantics that
the meaning of a lazy program comprises all of its nondeterministic evaluations
and the meaning can be refined later in light of new external information.

The equivalence of clairvoyant evaluation to the natural heap-based
definition of laziness <cit.> was proved by <cit.>:
the cost of any execution in clairvoyant call-by-value is an upper bound of the
cost in call-by-need, and there is some clairvoyant execution whose
cost is actually the same as in call-by-need.
In this paper, we carry on with the clairvoyant interpretation.

Taking the append function as an example (recall its definition
in <ref>), when it makes a recursive call, we fork
the evaluation into two branches: in branch (1), we perform the recursive
call; and in branch (2), we skip that call. A skipped call yields a placeholder
value as a result, which we call $\bot$ or Undefined.

Parts of the nondeterministic clairvoyant call-by-value evaluation of
the append function applied to two lists [1, 2, 3]
and [4].

Suppose that all future demands only require the first element of the result
list, then branch (2) would suffice for offering that result. However, if a
future demand requests more than that, branch (2) would fail to proceed because
the requested data is Undefined. Therefore, branch (2) would get stuck and
not yield any result at all. Fortunately, there would still be branch (1) to
return the result. Furthermore, in branch (1), the append function may
make another recursive call to itself, as long as the first argument list is not
nil. In that case, this branch would be once again forked into two
branches. This is illustrated by <ref>.

Although lazy programs are now interpreted nondeterministically, nondeterminism
is used in a very controlled manner.  The only choices we make are whether to
perform a computation or to skip it.  This means that the value of a program, if
it exists, is still unique in some sense: the only possible changes are that
parts of the value are replaced with Undefined.

If we know which branch leads to a successful evaluation for the append
function, we can just look at that branch and add its cost to obtain the total
cost of the program, which gives us a local reasoning methodology. Of course we
cannot know this in advance, but there are some reasoning principles that can

§.§ A Dual Reasoning Principle

We would like to have a reasoning methodology that is both local
and modular, just like what we would expect from functional
programming. This means that we should be able to use some relations to specify
the behaviors of each individual function. And when we want to reason about a
program, we can just do that by composing the relations of its functions.

We use a dual reasoning principle to achieve the locality and modularity for
clairvoyant call-by-value evaluation. First, we have a
specification that describes the behaviors of all of the function's
nondeterministic branches. The  specification can offer us an accurate
description of functional correctness under call-by-need evaluation. However,
the specification is  because it does not rule out the branches that
contain redundant steps and would not appear in an actual call-by-need

To be more selective in those branches, we use an  specification
that describes the behaviors on a specific branch. The specification is
because it can be used to specify a more accurate bound for the cost under
call-by-need evaluation.

<Ref> shows the relations among a clairvoyant evaluation,
a  specification, and an  specification.

The relations among a clairvoyant evaluation, a
specification, and an  specification. The tree in the middle of the
figure represents the nondeterminism tree of clairvoyant evaluation. The gray
nodes represent the end results of their branches. A  specification
specifies the nodes in the red circle. And an  specification
specifies the node in the blue circle.

Getting back to append, its  specification states:

For all the nondeterministic branches of the append function, if
the branch evaluates successfully, it will return a cost $c \in [1, \text{length
} xs + 1]$.

For simplicity, we omit the functional correctness part of the specification
here. The  specification only specifies a coarse range
for append's costs. If we want to reason about our earlier
example p, we could not deduce that its cost would never go over n
by reasoning about append and take abstractly using their
specifications. Instead, we can only deduce that the upper bound of the cost is
the length of xs, which may be much larger than n.

For this sort of analysis, we need the  specification of append:

For any number $n \in [1, \text{length }xs]$ (or $n \in [1, \text{length }xs +
1]$ if $xs$ does not contain any undefined part), [When $xs$ does not
contain any undefined part, append might go over the entire list and take
one extra cost pattern matching on nil. This is the only case the cost
of append will be bigger than the length of $xs$.] there exists a nondeterministic branch
of the append function that evaluates successfully and returns a cost $c =

A major difference between the  and the  specifications is that
the latter does not only show a range of costs; it shows what exactly are the
possible costs within this range. With the help of this specification, we can
“pick” one branch where the possible cost, which might be much smaller than
the length of $xs$, barely suffices for producing a list that take needs.

Both the  and  specifications can be proved on the append
function. And when reasoning about a larger program like p, all we need is
to compose the specifications of append with the specifications of other
functions like take.

§.§ The Missing Pieces

So far, we have informally discussed our methodology. The main missing piece to
develop in the rest of the paper is to implement this methodology in the formal
environment of the Coq proof assistant.

The first step is to associate the pure functional programs with versions that
track execution costs and allow nondeterminism. It turns out that we can do that
with monads <cit.>. In the next section, we define the
clairvoyance monad, which distills the main features of clairvoyant
evaluation. One attraction of the clairvoyance monad is its simplicity: its
core definitions consist of merely 21 nonblank, noncomment lines of code in
Coq. Then, we translate pure functions into the clairvoyance monad in <ref>.
The final step, in <ref>, is to build a program logic for the
clairvoyance monad that enables local and modular formal cost analysis in the
style of  and  specifications.

§ THE CLAIRVOYANCE MONAD

The clairvoyance monad (<ref>) is a lightweight
abstraction that can express the semantics of instrumented lazy evaluation,
suitable for cost analysis.  Based on the ideas of clairvoyant
evaluation <cit.>, its simplicity is largely due to the absence of
higher-order state commonly associated with laziness.

To model clairvoyant evaluation, we need a monad that can encode all the
following three ingredients: (1) costs, (2) nondeterminism, and (3) failures on
some nondeterministic branches. The clairvoyance monad is the simplest monad
that meets the criterion.

Core definitions of the clairvoyance monad M.

A computation in the clairvoyance monad, of type M a, nondeterministically
yields a value v : a after some time n.
A computation is defined as a set of such pairs (v, n), encoded in Coq as a
predicate a -> nat -> Prop.
The return of the monad yields the given value v with cost 0; it is
a set containing only (v, 0). The bind of the monad sequences computation by
getting a result (x, nx) from the first operand u, and then feeding the
value x to the continuation k, which then yields another
result (y, ny). The overall result is that latter value paired with the
total cost (y, nx + ny).

To track time, tick <cit.> is a computation with unit cost. This design follows the same
rationale as <cit.>: explicit ticks make the library lightweight
and flexible to experiment with different cost models.  For a given cost model,
one can ensure that ticks are added consistently by an automatic translation.
We present such a translation in <ref>.

The type of thunks T is structurally an option type. A thunk is
either a known value, under the Thunk constructor, or it is Undefined.
Undefined thunks are placeholders introduced when a computation is
“skipped,” because its result won't be needed.

For “laziness,” we add two operations to create and force thunks.
Intuitively, the thunk function stores a computation of type M a
without evaluating it, and yields a thunk: a reference to that stored
computation, of type T a. The forcing function looks up that reference
to evaluate the corresponding computation and passes it to the continuation. This result is
also stored in place of the computation, so that subsequent uses of force
will not recompute the result.

In the clairvoyance model, thunk's implementation nondeterministically
chooses between (1) running the computation, yielding any one of its results in
a Thunk, and (2) skipping it, yielding an Undefined result at no
cost.  The set of possible outcomes is implemented as a predicate: it accepts
any pair (Thunk v, n) such that (v, n) is accepted by the given
computation u and the pair (Undefined, 0).

The forcing operation accesses the result stored in a thunk and passes it
to a continuation. If there is indeed a value Thunk v, then v is the
result, and we just pass it to the continuation k. We do not need to add
any costs in this step: we already paid the cost of computing v on the
thunk's creation. If the thunk is Undefined, then the computation fails:
it has no result, as denoted by the empty set. Note that the only way to fail
among the above five combinators is to use forcing and that
thunk is the only way to produce thunks to apply forcing to.
In spite of this underlying potential for failure, computations definable with
these combinators always have at least one successful execution by never
skipping a thunk. In that sense, our combinators adequately model a total

The empty computation fun _ _ => False : M a could also be added to the
core definitions.  In this paper, we will stick to total functional
programming <cit.>.

When programming, we also rely on Coq notations for
a few well-known monadic operations in addition to these core definitions.
The infix notation “>>” abbreviates bind with a
constant continuation:

Notation "t >> s" := (bind t (fun _ => s)).

In the clairvoyance monad, a common idiom is tick >> t to increase the
cost of t by one.

Functions whose arguments are thunks are called lazy, in the sense that
their arguments may not always be defined. Otherwise they are eager.  Let
us define the following notations, wrapping the monadic bind in more
familiar syntax, akin to do-notation in Haskell and overloaded let in
OCaml.  The infix $! is named after a standard Haskell operator which
makes a function strict.  For reference, typing rules for these constructs are
given in <ref>.

Notation "let! x  := t in s" := (bind t (fun x => s)).
Notation "let  xA := t in s" := (bind (thunk t) (fun xA => s)).
Notation "f $! xA" := (forcing xA f).
\end{lstlisting}
We thus view the combinator \cdc{bind} as an ``eager'' \cdc{let!} construct,
where the bound variable \cdc{x} is the result of the computation \cdc{t}.  In
contrast, a composition of \cdc{bind} and \cdc{thunk} provides a ``lazy''
\cdc{let~}, where \cdc{xA} is a thunk for the ``delayed'' computation \cdc{t}.
In this paper, variables of ``lifted'' types \cdc{T a} will be marked with a
suffix \cdc{-A}, to constrast with variables of ``unlifted'' types \cdc{a}.

\begin{figure}
% https://tex.stackexchange.com/questions/562160/is-there-a-way-to-use-the-listings-package-together-with-mathpartirs-mathpar
\newcommand\zcdc[1]{\let\par\endgraf\cdc{#1}}
\begin{mathpar}
\inferrule
{\Gamma \vdash \hbox{\zcdc{t : M a}} \\
\Gamma, \hbox{\zcdc{(x : a)}} \vdash \hbox{\zcdc{s : M b}}
{\Gamma \vdash \hbox{\zcdc{let! x := t in s : M b}}}

\inferrule
{\Gamma \vdash \hbox{\zcdc{t : M a}} \\
\Gamma, \hbox{\zcdc{(xA : T a)}} \vdash \hbox{\zcdc{s : M b}}
{\Gamma \vdash \hbox{\zcdc{let~ xA := t in s : M b}}}

\inferrule
{\Gamma \vdash \hbox{\zcdc{f : a -> M b}} \\
\Gamma \vdash \hbox{\zcdc{xA : T a}}
{\Gamma \vdash \hbox{\zcdc{f \$! xA : M b}}}
\end{mathpar}
\caption{Typing rules for \cdc{let!}, \cdc{let~}, and \cdc{\$!}}\label{fig:notation-typing}
\end{figure}

The definition of \cdc{T} has two important features. First, a thunk is merely a
value, not an indirect location in a ``heap'' as it would be in natural
semantics~\cite{launchbury1993}; this is key to the simplicity of our
Second, the type constructor \cdc{T} can be used in inductive type declarations
and plays well with the strict positivity condition imposed on
This will be essential in the translation of recursive types
in \cref{sec:translation}.

In the clairvoyance model, it is useful to think of thunks as a way to construct
\emph{approximations}~\cite{scott76}. The type \cdc{T a} ``lifts'' a type
\cdc{a} with an \cdc{Undefined} value which approximates all values of type
\cdc{a}.  Recursive types may contain nested thunks, thus defining rich domains
of approximations. In the monad \cdc{M}, we view a lazy computation as producing
an approximation of some pure, complete result; more precise approximations
are more costly to compute. That structure will be made explicit in
\cref{sec:reasoning}.

\paragraph{Remark}
The monad \cdc{M} coincides with the writer monad
transformer~\citep{monad-transformers} applied to the powerset monad \cdc{_ ->
Prop}. This observation crisply summarizes the orthogonal roles of
nondeterminism and accounting for time in the clairvoyance monad.

\section{Translation}\label{sec:translation}

The clairvoyance monad provides us with an explicit model of laziness.
To reason about the cost of programs in a lazy language---where laziness is
implicit---we make computations explicit by translating them into monadic
programs. We present such a translation in this section. We will then introduce
a framework for reasoning about computations in the clairvoyance monad in the
next section.

Our source language is a total lazy calculus with folds, enabling structural
recursion. In practice, our programs are embedded in Gallina, a pure and total
language which does not prescribe an evaluation strategy---multiple evaluation
strategies are actually available. Hence, Gallina terms have no inherent
notion of cost. Our monadic translation defines a second embedding that
determines a lazy evaluation strategy, allowing us to reason about the cost of
lazy functional programs.

Totality is arguably not a strong limitation for implementing many algorithms:
in the context of complexity analysis, termination is a necessary condition
for defining the cost of an algorithm.

In this section, we formalize the source language and its translation to Gallina.
Our examples of source programs are embedded in Gallina, and we currently
translate them by hand.
This formalization will serve as the basis for a future implementation of a
translation from Haskell.

\subsection{Formal Monadic Translation}\label{sec:semantics}

We define a translation from a simply typed lambda calculus to Gallina using the
monad \cdc{M} and the definitions in \cref{fig:clairvoyance-monad}. The syntax
of the source calculus is summarized in \cref{fig:lambda-syntax}. A primitive
type of lists serves to illustrate how to translate algebraic data types, with
structural recursion modeled by a $$ operator.  This calculus is in
A-normal form~\cite{anf} to streamline the monadic translation by confining the
bookkeeping of thunks to $$ and $$.

\begin{figure}[t]
\begin{align*}
\emph{types}\qquad    & \tau  &\ ::=\ & \tau \to \tau \;|\; \listty\;\tau \;|\; \unitty \\
& x,y,z & \in\ & \textit{variables} \\
\emph{terms}\qquad    & t,u   &\ ::=\ & x \;|\; \lambda x.\,t \;|\; t\;x \;|\; \lettm{x}{t}{u} \\
&       &\ \;|\;& \niltm \;|\; \constm\;x\;y \;|\; \foldtm{t}{(\lambda x\, y. t)}{z}
\end{align*}

\begin{mathpar}
\inferrule
{\Gamma \vdash x : \listty\;\tau_1 \\
\Gamma \vdash t_l : \tau_2 \\
\Gamma,\, y_1 : \tau_1,\, y_2 : \tau_2 \vdash t_n : \tau_2
{\Gamma \vdash \foldtm{t_l}{(\lambda y_1 y_2. t_n)}{x} : \tau_2}
\end{mathpar}
\caption{Syntax and typing rules for $\foldsym$}
\label{fig:lambda-syntax}
\end{figure}

\newcommand\den[1]{\llbracket#1\rrbracket}

In the translation of types (\cref{fig:type-translation}),
source function types $τ_1 →τ_2$ are translated to
target function types $T τ_1 →M τ_2$.
The argument is wrapped in a thunk, so functions may be defined on undefined inputs.
And the result is, of course, a computation.
The type of lists is translated to an inductive type where fields are wrapped in a
thunk \cdc{T}. This type thus represents partially defined lists, which can be seen
as \emph{approximations} of actual lists.

In the translation of terms (\cref{fig:term-translation}),
a well-typed term $t : τ$ is translated to a Gallina term $t :
M τ$.  We pun source variables $x : a$ as target
variables $x : T a$.  A \cdc{tick} is added uniformly in the
interpretation of every non-value construct---this follows \citet{clairvoyant}:
it is assumed that those constructs will be implemented in constant time.  In
our examples, we will simplify ticks further, as discussed in
\cref{subsec:simplify-tick}.

Types guide the design of the term translation.
The source \cdc{Let} corresponds to our lazy \cdc{let~}, creating thunks,
while variable expressions $x : M τ$ force the
thunk denoted by the variable $x : T τ$.

The translation of $$ is defined in \cref{fig:foldr-def}.
A \cdc{tick} happens at every recursive call. And recursive calls are
thunked using the \cdc{let~} construct, so that they may remain unevaluated
if the \cdc{c} computation doesn't need them.

Recursion introduces a wrinkle in our translation. Generally, function
arguments $x : a$ are lifted to $x : T a$. However, recursive
definitions in Coq must take an argument whose outer type constructor
is defined using recursion, \cdc{listA a}, unlike the type of thunks \cdc{T (listA a)}.
Thus the translated \cdc{foldrA} is merely a wrapper around the recursive function
\cdc{foldrA'} where most of the work happens.
Moreover, in \cdc{foldrA'}, the subterm \cdc{x2} is forced in
continuation-passing style, using \cdc{forcing} (under the notation \cdc{\$!}),
in order to ensure that the recursive call to \cdc{foldrA'} is syntactically
applied to a subterm of the initial list \cdc{x'}.

\begin{figure}
\begin{minipage}{0.3\textwidth}
\begin{align*}
\den{\tau_1 \to \tau_2} &= \text{\cdc{T}}\;\den{\tau_1} \to \text{\cdc{M}}\;\den{\tau_2}
\\ \den{\listty\;\tau} &= \text{\cdc{listA}}\;\den{\tau}
\end{align*}
\end{minipage}
\quad
\begin{minipage}{0.5\textwidth}
\codeplus{example.v}{listA}{language=Coq}
\end{minipage}
\caption{Monadic type translation on the left; definition of \cdc{listA} on the right}\label{fig:type-translation}
\end{figure}

\begin{figure}
\begin{align*}
\den{\lettm{x}{t}{u}} &= \text{\cdc{tick >> let~}\;$x$\;\cdc{:=}\;$\den{t}$\;\cdc{in}\;$\den{u}$}
\\ \den{x} &= \text{\cdc{tick >> force}}\;x
\\ \den{\lambda x.t} &= \text{\cdc{ret (fun}\;$x$\;\cdc{=>}\;$\den{t}$\cdc{)}}
\\ \den{t\;x} &= \text{\cdc{tick >> let! f :=}\;$\den{t}$\;\cdc{in}\;\cdc{f}\;$x$}
\\ \den{\niltm} &= \text{\cdc{ret NilA}}
\\ \den{\constm\;x\;y} &= \text{\cdc{ret (ConsA}\;$x$\;$y$\cdc{)}}
\\ \den{\foldtm{t_l}{(\lambda y_1 y_2. t_n)}{x}} &= \text{\cdc{foldrA}\;$\den{t_l}$\;\cdc{(fun}\;$y_1$\;$y_2$\;\cdc{=>}\;$\den{t_n}$\cdc{)}\;$x$}
\end{align*}
\caption{Monadic term translation}\label{fig:term-translation}
\end{figure}

\begin{figure}
\codeplus{example.v}{foldr}{language=Coq}
\caption{Definition of the \cdc{foldrA} function used in the translation of $\foldsym$}
\label{fig:foldr-def}
\end{figure}

\subsection{Equivalence with Clairvoyant Call-By-Value}\label{subsec:compare-clairvoyant}

Our translation $·$ is a cost-aware denotational semantics for the simply-typed lambda calculus.
Formally, this semantics $t$ is parameterized by an
\emph{environment} $ρ$ that maps the free variables of $t$ to semantic
values. The denotation $t(ρ) : M τ$ is thus a
set of cost-value pairs $(n, v)$, with $n : ℕ$ and $v : τ$.

We have proved the equivalence between our denotational semantics
and \emph{clairvoyant call-by-value} evaluation, the operational semantics of
laziness introduced by \citeauthor{clairvoyant}, which itself was proved
equivalent to the natural semantics of \citet{launchbury1993}.
Clairvoyant call-by-value evaluation is defined as an inductive relation
$thnuh'$ expressing that the term $t$ with an
initial \emph{heap} $h$ evaluates, with cost $n$, to a \emph{value term} $u$
and a final heap $h'$.
To state this equivalence, we extend our denotation function $·$ to these auxiliary syntactic
constructs: a heap $h$, which maps variables to terms, denotes an environment
$h$, and a (syntactic) value term $u : τ$, in an environment $ρ$,
denotes a (semantic) value $u(ρ) : τ$.

We can now state an equivalence between our denotational semantics $·$
and the operational semantics $⇓^CV$:
\begin{theorem}
For any well-typed term $t$ and heap $h$, and for any value-cost pair $(v,n)$,
the following propositions are equivalent.
\begin{enumerate}
\item $(v,n) \in \den{t}(\den{h})$.
\item There exists $u$ and $h'$ such that $\ccbv{t}{h}{n}{u}{h'}$ and $v = \den{u}(\den{h'})$.
\end{enumerate}
\end{theorem}
The forward direction, (1) implies (2), states the \emph{adequacy} theorem:
the denotational semantics $·$ is a subset of the operational
semantics $⇓^CV$. Conversely, the backward direction, (2) implies (1),
states our \emph{soundness} theorem: all evaluations by the operational semantics produce denoted cost-values. Together, these
results prove that our semantics is equivalent to the operational semantics
of \citeauthor{clairvoyant}.

We have formalized both the denotational semantics $·$ and the
operational semantics $⇓^CV$ and proved the equivalence
theorem in Coq~\citep{forking-paths-artifact}. The proof, which proceeds by
induction on $n$ for adequacy and on derivations of $⇓^CV$
for soundness, is straightforward thanks to the simplicity of the language,
notably excluding general recursion. Most of the work is devoted to relating
mutable heaps $h$ in the operational semantics $⇓^CV$ to
environments $ρ$ in our denotational semantics $·$.

In addition to an operational semantics $⇓^CV$,
\citet{clairvoyant} also presented a denotational cost semantics, which we can
compare to ours.
First, the cost semantics of \citeauthor{clairvoyant} is defined for an untyped
recursive calculus and our translation is defined for a typed calculus with
folds---guaranteeing termination. However, since the clairvoyance monad is
based on the powerset monad \cdc{_ -> Prop}, we can also define a fixpoint
operator (an example is \cref{fig:fixpoint}):
\[ \hbox{\cdc{Fix : ((a -> M b) -> (a -> M b)) -> (a -> M b)}} \]
Such an operator could be used for the denotational semantics of a general
recursive lazy language, but at the cost of a more complex equivalence theorem.
The issue is that the unfolding lemma \cdc{Fix F <-> F (Fix F)} assumes the
monotonicity of \cdc{F}, adding a significant burden to using that operator.
Without using \cdc{Fix}, we have only modelled a total language, as the source
language we considered above is intended to be a subset of Gallina. Many
algorithms, in the functional programming literature especially, are defined
using various forms of structural recursion, so they can be embedded in our

\begin{figure}
\codeplus{example.v}{Fix}{language=Coq}
\caption{Possible fixpoint combinator in the monad \cdc{M}}\label{fig:fixpoint}
\end{figure}

Second, the denotations of \citeauthor{clairvoyant} are cost-value pairs that
inhabit a lattice to handle general recursion; they handle
nondeterminism by joining all executions together. However, in the denotation
of \textsc{Let}, the cost of evaluating the binding is discarded if the body of
the \textsc{Let} does not depend strictly on the binding. In comparison, our
semantics models computation using sets of pairs, so the cost of every
nondeterministic path is preserved.

Key to the simplicity of our approach, the core operations of our clairvoyance
monad~(\cref{sec:clairvoyance-monad}) are operations on sets; these operations do not rely
on an abstract lattice structure for values.  In exchange, our semantics is
less well-behaved: \cdc{let~} expressions with unused thunks generate spurious
approximations. We present a dual logic that disregards such uninformative
approximations in \cref{sec:reasoning}.

\subsection{An Example}\label{subsec:translation-example}

We show our translation in action on the example of \cdc{append} and \cdc{take},
illustrating a few pragmatic tweaks to our formalization above.  The source
program with pure functions in \cref{fig:source-example} is translated into the
monadic program in \cref{fig:translated-example}. For simplicity, we retain the
use of fixpoints instead of representing all recursion with \cdc{foldrA}.

These definitions use the \cd{listA} type from \cref{fig:type-translation}.
This type is the corresponding \emph{approximation type} for Gallina's
native \cd{list}, and wraps every field in the thunk type
constructor \cdc{T}.

\begin{figure}[t]
\codeplus{example.v}{trans}{language=Coq}
\caption{The translated code of \cdc{append} and \cdc{take} from the pure version of \cref{fig:source-example}.}\label{fig:translated-example}
\end{figure}

The translation of recursive functions follows a similar structure to the
definition of \cdc{foldrA} in the previous section, since \cdc{append}
and \cdc{take} are in fact specialized list folds (\cdc{foldr}): their
translations are wrappers for the recursive \cdc{append_} and \cdc{take_} where
pattern-matching happens, and the recursive calls are guarded by thunks.

We keep the primitive representation of certain types, such as \cdc{nat} in the
definition of \cdc{take}, instead of using its Peano representation.  The main
reason to do so is that it makes the resulting program simpler by denoting
``primitive'' operations more directly. Although this is generally unsound
for a language with pervasive laziness, this issue could be palliated by using a
strictness analysis to ensure that variables of that type are never instantiated
with $$.
Alternatively, we could consider a source language where both lifted and
unlifted types coexist---Haskell is actually such a language, although unlifted
types are not commonly used because GHC's strictness analysis is often good
enough to enable optimizations.

The \cdc{append} function, of type \cdc{list a -> list a -> list a}, is
translated to its approximate version \cdc{appendA}, of type
\cd{T (listA a) -> T (listA a) -> M (listA b)}.
In other words, the arguments are put under thunks \cdc{T},
and the result is produced by an explicit computation \cdc{M}.
This differs slightly with our formal translation where we simply translated a
term $t : τ$ to $t : M τ$.
We can do away with that outer \cdc{M} because, typically, top-level functions
are values.

Finally, we translate the bodies of the functions. To match the syntax of
\cref{fig:lambda-syntax}, we sequentialize expressions to ANF~\citep{anf} (if they are not already in this form), so that every
computation happens at a \textsc{Let} binding. We then translate the ANF
program to a monadic program, following \cref{fig:term-translation}.

With the translated code, we can now formally analyze its cost. We will show how
we specify its cost and how we reason about that in \cref{sec:reasoning}.

\subsection{Simplifying Ticks}\label{subsec:simplify-tick}
In our examples, we have simplified the translated code further to only
keep a single \cdc{tick} at the head of source function bodies. This incurs a
change to the cost of computations bounded by a multiplicative constant of the
original cost. Considering that those costs are purely abstract quantities
to begin with, this seems an acceptable trade-off to make the translated code
more readable.

This simplification can be broken down in two steps. First, apply the following
rewrite rules to ``float up'' every \cdc{tick} in every subexpression:
\[
\hbox{\cdc{bind t (fun x => tick >> k x) = (tick >> bind t k)}}
\]
\[
\hbox{\cdc{thunk (tick >> u) <= (tick >> thunk u)}}
\]
where the inequality \cdc{<=} means in this context that every execution
\cdc{(x, nR)} on the right-hand side corresponds to an execution \cdc{(x, nL)}
on the left-hand side with the same result but a lower or equal cost \cdc{nL <=
nR}.~\footnote{The equality should be interpreted as extensional equality. We
have formally proved these rewrite rules in Coq~\citep{forking-paths-artifact}.}
That rewriting may increase the cost of programs, which is fine since we are
eventually most interested in finding upper bounds on that cost.  Second, once
all ticks are as high in the program as they can be, we replace all consecutive
ticks with a single one. The resulting ``speed-up'' of the computations is
bounded by a constant multiplicative factor equal to the longest chain of ticks
substituted that way.

\section{Formal reasoning}\label{sec:reasoning}

A guiding principle in designing our methodology is to have reasoning rules that
are both \emph{local} and \emph{modular}. By local, we mean that we can reason
about each function independently; and by modular, we mean we can reason about
the whole program by composing the results of reasoning about its parts.

However, in doing so we face a challenge: clairvoyant call-by-value
evaluation is an \emph{over-approximation} of call-by-need evaluation: it
contains nondeterministic branches that would not appear in an actual
call-by-need evaluation.
Therefore, to reason precisely about call-by-need
execution, we need reasoning rules that are \emph{general} enough to contain
many nondeterministic results, but also \emph{selective} enough to prune
nondeterministic branches that contain redundant steps.

We address this challenge with a dual specification
methodology. For \emph{generality}, a \emph{\pessim} specification talks about
the behaviors on all nondeterministic branches.  For \emph{selectiveness},
an \emph{\optim{}} specification describes the behavior of specific
branches.~\footnote{All the theorems discussed in this section have been
formally proved in Coq and they are available in our

\subsection{The \Optim{} and \Pessim{} Specifications}

The definitions of the \pessim{} specification and the \optim{} specification
are shown in \cref{fig:spec-defs}. Both are parameterized by a \emph{specification relation}
\cdc{r : a -> nat -> Prop} which specifies a set of desired values and costs.
A \pessim{} specification states that all nondeterministic branches of the
program \cdc{u} satisfy the relation \cdc{r}.  On the other hand, the
\optim{} specification requires the existence of \emph{at least one}
nondeterministic branch satisfying the relation \cdc{r}.

We use the following notations to denote these two kinds of
specifications:~\footnote{We omit the Coq notation levels in the code.}
\begin{lstlisting}[language=Coq]
Notation " u {{ r }} " := (pessimistic u r).
Notation " u [[ r ]] " := (optimistic  u r).
\end{lstlisting}

\begin{figure}[t]
\codeplus{example.v}{pess/opt}{language=Coq}
\caption{The definitions of the \pessim{} and \optim{} specifications.}\label{fig:spec-defs}
\end{figure}

\subsection{Reasoning Rules}

We can define a set of reasoning rules for the \pessim{} specification and
the \optim{} specification, respectively. For each kind of specification, we
build some reasoning rules for the five basic monadic combinators
(\cdc{ret}, \cdc{bind}, \cdc{tick}, \cdc{thunk}, and \cdc{forcing}) described
in \cref{sec:clairvoyance-monad}. We can then reason about our programs purely
based on these reasoning rules plus a monotonicity rule.

\newcommand\pessimr[2]{#1\ {\colorPessim\{\!\{}\ #2\ {\colorPessim\}\!\}}}
\newcommand\optimr[2]{#1\ {\colorOptim[[}\ #2\ {\colorOptim]]}}

\begin{figure}[t]
\begin{mathpar}
\inferrule
{r\ x\ 0}
{\pessimr{(\texttt{ret}\ x)}{r}}

\inferrule
{\pessimr{u}{\lambda x\ n. \pessimr{(k\ x)}{\lambda y\ m. r\ y\ (n + m)}}}
{\pessimr{(\texttt{bind}\ u\ k)}{r}}

\inferrule
{r\ \texttt{tt}\ 1}

\inferrule {\pessimr{u}{r} \\ \forall x\ n, r\ x\ n \rightarrow r'\ x\ n}
{\pessimr{u}{r'}} {\hbox{monotonicity}}

\inferrule
{r\ \texttt{Undefined}\ 0 \\
\pessimr{u}{\lambda x. r\ (\texttt{Thunk}\ x)}}
{\pessimr{(\texttt{thunk}\ u)}{r}}

\inferrule
{\forall x, t = \texttt{Thunk}\ x \rightarrow \pessimr{(k\ x)}{r}}
{\pessimr{(k\ \texttt{\$!}\ t)}{r}}

\inferrule
{\pessimr{u}{r} \\ \pessimr{u}{r'}}
{\pessimr{u}{\lambda x\ n.r\ x\ n\ \wedge\ r'\ x\ n}}
\end{mathpar}
\caption{Reasoning rules for \pessim{} specifications.}\label{fig:pessim-reasoning}
\end{figure}

\begin{figure}[t]
\begin{mathpar}
\inferrule
{r\ \texttt{Undefined}\ 0 \ \vee\  \optimr{u}{\lambda x. r\ (\texttt{Thunk x})}}
{\optimr{(\texttt{thunk}\ u)}{r}}

\inferrule
{t = \texttt{Thunk}\ x \\ \optimr{(k\ x)}{r}}
{\optimr{(k\ \texttt{\$!}\ t)}{r}}

\inferrule
{\pessimr{u}{r} \\ \optimr{u}{r'}}
{\optimr{u}{\lambda x\ n.r\ x\ n\ \wedge\ r'\ x\ n}}
\end{mathpar}
\caption{Reasoning rules for \optim{} specifications. We omit the rules
for \cdc{ret}, \cdc{bind}, and \cdc{tick} as well as the monotonicity rule
because these rules have the same forms as those of the \pessim{}
\end{figure}

\Cref{fig:pessim-reasoning} shows the reasoning rules for \pessim{}
specifications. \cdc{ret x} satisfies the \pessim{} specification \cdc{r} if the
result \cdc{x} and the cost 0 are in the set of \cdc{r}. \cdc{bind u k}
satisfies the \pessim{} specification \cdc{r} if all the results of \cdc{u} can
be composed with the continuation \cdc{k} such that all the final results are in
the set of \cdc{r}. A \cdc{tick} satisfies the \pessim{} specification \cdc{r}
if \cdc{tt}~(the only value of the \cdc{unit} data type in Coq) and 1 are in the
set of \cdc{r}. We also need a monotonicity rule to relax the \pessim{}
specification relation and a conjunction rule to combine \pessim{}

The term \cdc{thunk u} satisfies the \pessim{} specification \cdc{r} if both
nondeterministic branches forked off from it satisfy the
relation \cdc{r}. The \cdc{forcing} rule requires that its continuation \cdc{k}
satisfies the relation \cdc{r} when applied to the value contained in
a \cdc{Thunk}; in the case that there is no defined value within the thunk (\ie
forcing an \cdc{Undefined}), the \pessim{} specification is vacuously satisfied
because the computation branch fails.

\Cref{fig:optim-reasoning} shows the reasoning rules for \optim{}
specifications. We omit the rules for the \cdc{ret}, \cdc{bind}, and \cdc{tick}
operators and the monotonicity rule here because they have the same form as
those of the \pessim{} specification. There are two ways to give an \optim{}
specification for \cdc{thunk} terms, corresponding to selecting one of the two
different nondeterministic branches that forked off from the \cdc{thunk}. In the
branch where the computation is skipped, we only need to show
that \cdc{Undefined} and 0 are in the relation \cdc{r}. In the branch where the
computation is evaluated, we show that there exists a result in the
computation \cdc{u} such that wrapping it in a \cdc{Thunk} constructor satisfies
the relation \cdc{r}. The \cdc{forcing} rule requires its argument to be a
defined value because forcing an \cdc{Undefined} results in failure. When
reasoning about a program, we need to select the proper \optim{} rule
at \cdc{thunk}s so that forcing an \cdc{Undefined} value never happens.

The conjunction rule for the \optim{} specification is also slightly different
because its premises require both a \pessim{} specification and an \optim{}

\subsection{Approximations}\label{sec:approx}

Before showing how we use both the \pessim{} and the \optim{} specifications
for reasoning about lazy programs, we need to answer this question: in what
sense does an approximation function implement a pure function?

Recall the approximation types and pure types discussed
in \cref{subsec:translation-example}. We would like to base our specification on
pure types, as this is what we normally write as functional programs. On the
other hand, our implementation in the clairvoyance monad uses approximation

We can connect these approximation and pure types together.  First observe
that we can inject pure types into partial types by thunking each subterm.
We call the result an \emph{exact} approximation because it constructs an
approximation which represents \emph{exactly} the original list.

\begin{lstlisting}[language=Coq]
Definition exact : list a -> listA a.
\end{lstlisting}

We cannot go the opposite way with a function, since approximations generally
contain less information than a full list. Instead, we generalize \cdc{exact}
as a relation \cdc{is_approx xsA xs} between a pure list \cdc{xs} on
the right and any of its approximations on the left. A notation turns
it into an infix operator with syntax inspired by Haskell.

\begin{lstlisting}[language=Coq]
Definition is_approx : listA a -> list a -> Prop.
Infix "`is_approx`" := is_approx.
\end{lstlisting}

Approximations themselves are partially ordered, when the second is at least
as defined as the first. We also use infix notation for this relation.

\begin{lstlisting}[language=Coq]
Definition less_defined : listA a -> listA a -> Prop.
Infix "`less_defined`" := less_defined.
\end{lstlisting}

In our running example using lists, we also simplify things by using the same
type \cdc{a} as the type of elements for pure lists \cdc{list a} and list
approximations \cdc{listA a}.

More generally, we want to overload the function \cdc{exact} and relations \cdc{is_approx} and
\cdc{less_defined}, so that (1) their names can be reused for user-defined data
types, (2) they are automatically lifted through the thunk type constructor \cdc{T}.

Some properties describe and relate these three relations formally. These
relations must be defined and their properties must be proved for every
user-defined approximation type; those propositions and their proofs (which we
omit) follow a common structure, so we conjecture that they can be automated.

The \cdc{less_defined} relation is an order relation.

\label{prop:less-defined-order}
\begin{lstlisting}[language=Coq]
Proposition less_defined_order : Order less_defined.
\end{lstlisting}

The set of approximations for a pure value is downward closed.

\label{prop:approx-down}
\begin{lstlisting}[language=Coq]
Proposition approx_down :
xsA `less_defined` ysA -> ysA `is_approx` xs -> xsA `is_approx` xs.
\end{lstlisting}

The list \cdc{xsA} is an approximation of \cdc{xs} if and only if \cdc{xsA} is
less defined than the exact approximation of \cdc{xs}.

\label{prop:approx-exact}
\begin{lstlisting}[language=Coq]
Proposition approx_exact : xsA `is_approx` xs <-> xsA `less_defined` (exact xs).
\end{lstlisting}

Exact approximations are maximal elements for the \cdc{less_defined} order.

\label{prop:exact-max}
\begin{lstlisting}[language=Coq]
Proposition exact_max : exact xs `less_defined` xsA -> exact xs = xsA.
\end{lstlisting}

A reference implementation of all the definitions shown in this section as well
as proofs for the above propositions on thunks and lists can be found in our
public artifact~\citep{forking-paths-artifact}.

\subsection{Functional Correctness}\label{sec:fun-correct}

To say that our approximation function implements the pure specification,
we would like two notions of correctness: (1)~a \emph{partial correctness}
notion that requires all the nondeterministic results of the approximation
function to be approximations of the result of the pure function; and (2)~a
\emph{pure correctness} notion that states the existence of a maximal
approximation result that is exactly the pure function's result.

We define the partial correctness of a function using the \pessim{}
specification, and the pure correctness of a function using the \optim{}
specification. For example, the partial and pure specifications
of \cdc{appendA}~(\cref{subsec:translation-example}) are shown
in \cref{fig:fcorrectness}. Given approximations of two input lists \cdc{xs}
and \cdc{ys}, \cdc{appendA} always, \ie pessimistically, yields an approximation
of \cdc{append xs ys}.
On the other hand, \cdc{appendA} optimistically yields exactly the
list \cdc{append xs ys} when applied to the exact approximations of \cdc{xs}
and \cdc{ys}. Both theorems can be proved by an induction over \cdc{xs}.

\begin{figure}[t]
\begin{lstlisting}[language=Coq]
Theorem appendA_correct_partial {a} :
forall (xs ys : list a) (xsA ysA : T (listA a)),
xsA `is_approx` xs -> ysA `is_approx` ys ->
(appendA xsA ysA) {{ fun zsA _ => zsA `is_approx` append xs ys }}.

Theorem appendA_correct_pure {a} :
forall (xs ys : list a) (xsA ysA : T (listA a)),
xsA = exact xs -> ysA = exact ys ->
(appendA xsA ysA) [[ fun zsA _ => zsA = exact (append xs ys) ]].
\end{lstlisting}
\caption{Definitions of \emph{partial} functional correctness and \emph{pure} functional correctness.}\label{fig:fcorrectness}\label{fig:partial-fun-correct}
\end{figure}

\subsection{Cost Specifications}\label{sec:cost-specification}

In this section, we show how we use both the \pessim{} and the \optim{}
specifications for reasoning about computation costs.

Using \cdc{appendA} as our running example, we first start with a \pessim{}
Since a \pessim{} specification describes all the nondeterministic branches of
a clairvoyant call-by-value evaluation, it might contain spurious branches which
overapproximate call-by-need evaluation too much. Thus, it can only offer a
loose upper bound for the computation cost.
Nevertheless, it is useful in specifying the lower bound,
while we can rely on an \optim{} specification to tighten the bounds.

Taking the \cdc{appendA} function~(\cref{fig:translated-example}) again as our
example, we can give it a \pessim{} specification as follow:
\codeplus{example.v}{appendA_cost_interval}{language=Coq}
The \cdc{xsA} and \cdc{ysA} passed to the \cdc{appendA} function are
approximations of the pure values \cdc{xs} and \cdc{ys}.

The size of approximation lists, defined in \cref{fig:sizex}, is a function
intended purely for reasoning, hence we name it \cdc{sizeX}, with a different
suffix from implementations such as \cdc{appendA}.  It is also parameterized by
the ``size'' of \cdc{NilA}, which is 0 or 1 depending on whether its presence
matters for a given specification.  Here, the extra unit of time accounts for
the final call to \cdc{appendA} which matches on \cdc{NilA}.

\begin{figure}
\begin{lstlisting}[language=Coq]
Fixpoint sizeX {a} (n0 : nat) (xs : T (listA a)) : nat :=
match xs with
| Thunk NilA => n0
| Thunk (ConsA _ xs1) => S (sizeX n0 xs1)
| Undefined => 0
\end{lstlisting}
\codeplus{example.v}{isdefined}{language=Coq}

\caption{Definition of \cdc{sizeX}\protect\footnotemark\ and \cdc{is_defined}.}\label{fig:sizex}\label{fig:isdefined}
\end{figure}

\footnotetext{Simplified for clarity. This is actually ill-formed
because the type \cdc{T (listA A)} is not a recursive type
(cf. \cref{sec:semantics}).}

A problem with this specification is that it only gives a range of the
computation costs. During the actual evaluation of the function \cdc{p},
the \cdc{takeA} function would never require more than the first \cdc{n}
elements of \cdc{appendA}'s resulting list, but this specification
of \cdc{appendA} fails to reflect that. We will only be able to compute that the
combined cost has a lower bound of $3$ and an upper bound of $(sizeX
1 xsA) + n + 1$, while in an actual call-by-need evaluation, the
cost would never exceed $2n + 1$.~\footnote{Note that the size
of \cdc{xsA} can be bigger than \cdc{n} if it is required with a higher demand

To address this problem, we give an \optim{} specification to \cdc{append}.
A first version states that \cdc{appendA} reaches the lower bound of the
interval in at least one execution.
\codeplus{example.v}{appendA_whnf_cost}{language=Coq}
The execution of \cdc{appendA} which satisfies that specification immediately
discards the computation in the \cdc{let~}, producing only a result in WHNF.

That specification could be strengthened to an equality \cdc{cost = 1}.
However, it is important to remember that results \cdc{(zsA, cost)} of a
clairvoyant computation are formal approximations of the behavior of a lazy
program. \cdc{zsA} is an approximation of the function's result, and \cdc{cost}
is an upper bound on its actual cost. Hence, only upper bounds on \cdc{cost} are
meaningful in \optim{} specifications, while \pessim{} specifications can assert
both lower and upper bounds. For that reason, we leave specifications
of \cdc{cost} as inequalities even though the simple specifications in this
section are technically valid with equalities. Note also that \pessim{} upper
bounds are quite fragile; they can be broken simply by adding spurious thunks in
a program.

Optimistic specifications about a single result such as \cdc{appendA_whnf_cost}
are unhelpful in most proofs, of course. A more expressive way to phrase
\optim{} specifications is to set an arbitrary \emph{demand}, raising the cost

Examining executions of \cdc{appendA} more closely, we can distinguish two
phases, with separate specifications. Before reaching the end of the first list
\cdc{xsA}, \cdc{appendA} computes an approximation of length \cdc{n} in time
\cdc{n}, for any \cdc{n} smaller than the size of \cdc{xsA}.
\codeplus{example.v}{appendA_prefix_cost}{language=Coq}

The natural number \cdc{n} represents an explicit demand on the output of
\cdc{appendA xsA ysA}: we demand an approximation with \cdc{n} constructors
\cdc{ConsA}, costing at most \cdc{n} units of time.

Another specification describes the execution of \cdc{appendA} that reaches
the end of the first list, yielding the most defined result---limited only by
the possible partiality of \cdc{ysA}. As a necessary condition, \cdc{xsA} must
be an exact approximation---modulo the definedness of its elements. Once we
reach the end of the list \cdc{xsA}, the thunk \cdc{ysA} will be forced, so we
require it to be defined, using the \cdc{is_defined} predicate in
\cref{fig:isdefined}. This guarantees that \cdc{zsA} will be defined past the
end of \cdc{xsA}, as specified by assigning a nonzero size to \cdc{NilA} in
applications of \cdc{sizeX}.%
\footnote{The \cdc{(xsA := exact xs)} binding in the following snippet is
desugared into a local definition using \cdc{let}.}
\codeplus{example.v}{appendA_full_cost}{language=Coq}

Natural numbers are not the most precise model of demand on lists: one may also
specify whether and to what extent the elements of the list in the first field
of \cdc{ConsA} constructors should be evaluated. In fact, approximation
types such as \cdc{listA} are the most general way to model demand.
However, when list elements are not explicitly used, a natural number is enough
to formalize the main aspects of complexity analysis for list operations.

\section{Case study: tail recursion}\label{sec:case-study}

We have already demonstrated our methodology on the program described in
\cref{sec:example}. Here, we show how to apply this approach in another context:
reasoning about functions written with tail recursion.~\footnote{All the
theorems discussed in this section have been formally proved in Coq and the
proofs are available in our artifact~\citep{forking-paths-artifact}.} Tail
recursion is a common optimization technique in the context of an eager
semantics. However, it can be a cause of performance degradation if not used
properly under lazy evaluation.

\paragraph{Tail Recursive \cdc{take}}
Consider a tail recursive version of the \cdc{take} function from
\cref{sec:example}, called \cd{take'}.  The key difference is the addition of
an accumulator to its parameters:
\codeplus{example.v}{take'}{language=Coq}
Even though the list must be reversed in the base case, \cdc{take'} is
better in an eager programming language because the
compiler can eliminate stack allocation~\citep{tail-modulo-cons}.

However, the original version is better for lazy evaluation, even if we ignore
the cost of \cdc{rev}. To get an intuition of why, consider the case where we
only demand the WHNF of the resulting list. This variant \cdc{take'} must go
over $n$ elements of the list before it returns the accumulator. In comparison,
the original \cdc{take} can immediately reveal the first element of the
resulting list in any of its pattern matching branches.

\paragraph{A Formal Analysis}
With the help of formal reasoning, we can better understand these functions'
difference from their specifications. In the specifications below, we axiomatize
the cost of \cdc{rev} used in \cdc{take'_} to have a cost of 0~\footnote{The
axiom would not make Coq's logic unsound because we can define such a function
in the clairvoyance monad by not inserting \cdc{tick}s.}. We introduce this
axiom so we can compare only the costs incurred by the recursive calls
on \cdc{take'_} and \cdc{take}. With this set up, let's look at the \pessim{}
specification of \cdc{take'A_}, the version of \cdc{take'_} written in the
clairvoyance monad:~\footnote{For simplicity, we omit the functional correctness
parts of the specifications in this section.}
\codeplus{example.v}{take'A_pessim}{language=Coq}
The \pessim{} specification describes a rather precise cost on all the
nondeterministic branches of \cdc{take'A_}. Furthermore, the cost is purely
decided by the pure values \cdc{n} and \cdc{xs}---the fact that the cost does
not depend on the actual approximations \cdc{zsA} output by \cdc{take'A_} is a
sign that the function may not be making effective use of laziness.

However, to show that \cdc{take} is better than \cdc{take'}, we need to
show that \cdc{take} can cost less than \cdc{take'}. What specification should
we use to show that? One possibility is the \pessim{} specification.
If we take this approach, we can show that the cost of \cdc{takeA}~(\cdc{take}
in the clairvoyance monad) is upper bounded by \cdc{n} and the size of the approximation \cdc{xsA}:
\codeplus{example.v}{takeA_pessim}{language=Coq}
Since approximations are always smaller than their pure values, the cost
shown here is smaller than that of \cdc{take'A_}---\emph{if} such costs indeed
exists. Unfortunately, the \pessim{} specification, which quantifies universally over all
executions, does not guarantee the existence of an execution. In fact, \cdc{take'A}
admits no execution at all if its arguments are not sufficiently defined,
so it satisfies the above specification vacuously.

To show the existence of certain costs, we need an \optim{} specification:
\codeplus{example.v}{takeA_optim}{language=Coq}

The \pessim{} specification of \cdc{take'A_} and the \optim{} specification
of \cdc{takeA} help unveil the key difference between these two: \cdc{take'A_}
does not make effective use of laziness, while the cost of \cdc{takeA} scales
with its demand.

\paragraph{List Reversal}
On the other hand, there are functions like \cdc{rev} that do benefit from
tail recursion. Consider a naive version without tail recursion:
\codeplus{example.v}{rev'}{language=Coq}
And the version with tail recursion:
\begin{lstlisting}[language=Coq]
Fixpoint rev_ {a} (ys : list a) (xs : list a) : list a :=
match xs with
| nil => ys
| x :: xs => rev_ (x :: ys) xs

Definition rev {a} (xs : list a) : list a := rev_ nil xs.
\end{lstlisting}
One reason that the non-tail-recursive version is worse is that \cdc{append} has
a non-constant cost, which leads \cdc{rev} to have a cost which grows quadratically
in the length of the input list. However, even if we imagine a constant time
version of \cdc{append} (\eg difference lists~\citep{difference-list},
catenable lists~\citep{purely-functional}), this version would not be
better than the tail-recursive one.~\footnote{If we consider the stack usage and
compiler optimizations, the tail-recursive version would be generally more
efficient and does not risk causing stack overflow.} Intuitively, this is
because both versions need to traverse the entire list \cdc{xs} to return the first
element of the resulting list, which is the last element of the input list.

Again we can inspect these two versions of \cdc{rev} formally to better
understand their difference.
Like above, we axiomatize \cdc{append} to have a cost of 0 so that our analysis
only considers the cost incurred by the recursive calls of \cdc{rev_}
and \cdc{rev'}. This simplification makes \cdc{rev'} cost less but will only
strengthen our claim that \cdc{rev'} would not beat \cdc{rev}.

First, we can show a rather specific cost with the \pessim{} specification
of \cdc{revA}:
\codeplus{example.v}{revA_pessim}{language=Coq}
In that specification, the cost is associated with the pure input value,
and is independent of the output value, which suggests that \cdc{revA} does not
make use of laziness. Indeed, this is true: we must iterate over the entire
list \cdc{xs} to get the first element of the resulting list.

We can also prove that \cdc{rev'A} satisfies the following \pessim{}
\codeplus{example.v}{rev'A_pessim}{language=Coq}
This specification shows that the cost of \cdc{rev'A} also does not depend the
approximations of \cdc{xs}, confirming our intuition that \cdc{rev'A} must also
iterate over the entire list.

\paragraph{Left and Right Folds}
One famous example concerning laziness is the difference between \cdc{foldl}
and \cdc{foldr}. While it seems that the major difference is just their
directions of folding, they actually have rather different costs. For
simplicity, let's only consider these operations on \cdc{list}s. The definitions
of \cdc{foldl} and \cdc{foldr} are shown below:
\codeplus{example.v}{folds}{language=Coq}

A formal analysis of these functions must also consider the cost of the
function \cdc{f} passed into them. For simplicity, let's assume that \cdc{f} has
a cost of only $1$. We can then prove that the translated versions of the above
two functions satisfy the following \pessim{} specification:
\codeplus{example.v}{foldl_pessim}{language=Coq}
\codeplus{example.v}{foldr_pessim}{language=Coq}

The \pessim{} specifications suggest that \cdc{foldrA} makes better use of
laziness because its cost is bounded by the length of approximation \cdc{xsA}.
However, as we have discussed earlier, we need to show that there are indeed
costs lower than the lower bound of \cdc{foldlA} that exists in some
nondeterministic branches of \cdc{foldrA}. For that, we once again need to show
the \optim{} specification of \cdc{foldrA}:
\codeplus{example.v}{foldr_optim1}{language=Coq}
\codeplus{example.v}{foldr_optim2}{language=Coq}
This concludes that, under lazy evaluation, \cdc{foldl} and \cdc{foldr} have the
same worst-case cost, but \cdc{foldr} has a lower cost if the demand is lower.

\section{Discussion}\label{sec:discussion}

\paragraph{Nondeterminism Monads}
The clairvoyance monad is not the only way to model nondeterminism; the list
monad is another possibility which allows some of these ideas to be implemented
without dependent types---necessary for \cdc{exists} and \cdc{eq}. Furthermore,
the list monad makes clairvoyant computations actually executable. We only
require a notion of choice and emptiness for programming; for reasoning, we need
some theory of membership \cdc{member : M a -> a -> Prop}, which defines a monad
morphism into the powerset monad.  This suggests that choosing the powerset
monad as we do here yields the simplest definitions.

\paragraph{Recursive \textsc{Let}}
A recursive \textsc{Let} for data types is yet another challenge.
It allows the construction of certain infinite structures by ``tying the knot'', such
\begin{center}
\cdc{ones = 1 :: ones} \quad\quad and\quad\quad \cdc{fib = 0 :: 1 :: zip_with plus fib (tail fib)}
\end{center}
However, these represent only a small fraction of programs manipulating
infinite structures, and there are many others, which do not rely on
recursive \textsc{Let}, that our reasoning framework can already handle.
For instance, the coinductive versions of \cdc{append} and \cdc{take} are
also actually modeled by our functions translated from the inductive
versions~(\cref{fig:translated-example}), by viewing our inductive \cdc{listA}
also as an approximation type for infinite lists.

In Haskell, \textsc{Let} is always recursive, but it is so rarely useful for
constructing data (as opposed to functions) that the shadowing it introduces is
often considered undesirable, and there is at least one proposal to disable

\section{Related Work}\label{sec:related-work}

\paragraph{Clairvoyant Evaluation}
Clairvoyant evaluation was first characterized by \citet{clairvoyant}. The main
inspiration for our paper, this work presented an operational semantics for
laziness as an alternative to the natural semantics of \citet{launchbury1993},
as well as a denotational cost semantics, following precursory ideas
by \citet{maraist1995}. We have compared our translation with the semantics
of \citeauthor{clairvoyant} as well as established an equivalence relation
between them in \cref{subsec:compare-clairvoyant}.

\paragraph{Monadic Translation}

\citet{moggi-monad} uses monads to describe computational effects and defines
various translations corresponding to different calling
conventions. \citet{wadler-monad} follows and describes the
translations for the call-by-value and call-by-name semantics, but leaves the
translation for call-by-need as an open problem. \citet{monad-recursive-types}
further adds positive inductive and coinductive types to these

\citet{malias} proposes a monadic translation that can be used under all
three different calling conventions, generalizing \citet{wadler-monad}, by
defining a function called \cdh{malias} which would be given different meanings
under different
semantics. In particular, \cdc{malias : M a -> M (M a)} is closely related to
our function \cdc{thunk : M a -> M (T a)}: it occupies the
same position in the translation of $$. The main difference is that,
whereas \cdc{malias} wraps thunks in computations; we expose thunks \cdc{T} as a
separate type.  In fact, we could define \cdc{malias t = bind (thunk t) force}
to hide thunks as well.  However, exposing \cdc{T} is crucial for use
in nested recursive type declarations; using \cdc{M} instead would violate
Coq's strict positivity condition. Furthermore, in \citet{malias}, \cdc{M} is
defined using Haskell's \cdc{ST} monad, relying on a polymorphic interface of
mutable references to represent the heap. We believe that it would be challenging to
emulate such an interface in Coq.

\paragraph{Computation Cost and Laziness}

There is much work on reasoning formally about computation costs.
For example, \citet{danielsson-08, lambda-amor, raml, implicit-complexity,
resource-bound-certification, timl} study intrinsic approaches to formal cost
analysis. Our work is in the extrinsic context of an interactive proof assistant.

On the extrinsic side, \citet{amortized-union-find, a-fistful-of-dollars} use
separation logic for reasoning about computation costs under call-by-value
evaluation using amortized analysis. Compared to these works, our goal of
reasoning about lazy pure functional programs does not require separation
Cost specifications could be made more modular by hiding
implementation-specific constant factors and formulating costs in asymptotic
terms. Works on formalizing asymptotic complexity
include \citet{asymptotic-complexity, asymptotic-proof-assistant,cutler20}.

\Citet{danielsson-08, liquidate} reason about lazy functional programs in a
monadic syntax annotated with ticks. An issue in both works is that they require
an explicit notion of laziness to model sharing: for example, in practice, a
list that is evaluated once will not be evaluated again under lazy
evaluation. To avoid a ``double counting'' of the cost in a thunk, a \cdc{pay :
nat -> M a -> M (M a)} combinator with an explicit representation of cost must
be annotated in the code~\footnote{The \cdc{pay} combinator is also an annotated
version of \cdc{malias : M a -> M (M a)}~\cite{malias}.}. This prevents both
works to be fully extrinsic in reasoning about laziness. With the clairvoyance
monad, thunks are either paid for or discarded immediately, so it is impossible
to count the cost of a thunk twice. This enables us to translate pure lazy
functions mechanically to monadic programs, and our proofs are completely

On the automated reasoning side, \citet{contract-based-lazy} verify a purely
functional subset of Scala by translating higher-order functions to first-order
programs via defunctionalization. They also model memoization by encoding the cache
as an expression that changes during the execution of the program.

For testing lazy functions in Haskell, Sloth is a tool that automatically
generates test cases to check if a function is ``unnecessarily
strict''~\citep{sloth}.  This tool relies on a ``less-strict'' ordering of
functions. One function is less-strict than another when, given the same input,
its result is less defined~\citep{less-strict}.

\Citet{foner2018} develop a library that generates random demands on the output
of a function and instruments inputs to record induced demand. Demands take the
form of approximations whose structure is also derived from pure data types.

\paragraph{Haskell}
Although we only discuss Coq here, Haskell is also a potential target of our approach.

The \hstocoq tool automatically translates Haskell programs to
Gallina---Coq's specification language---using shallow
embeddings~\citep{hs-to-coq}. It has been used for verifying a significant
portion of Haskell's \cdc{containers} library~\citep{containers} and one part of
GHC~\citep{verify-ghc}. However, \hstocoq's pure translation cannot be
used for cost analysis so existing work using this tool has been restricted to
functional correctness.

\Citet{haskell-monadic-translation} and \citet{one-monad} respectively translate
Haskell to monadic embeddings in Agda and Coq, based on the call-by-name
translation by \citet{moggi-monad}. This is enough to model Haskell's
partiality, but not its lazy cost semantics.

\LiquidHaskell augments Haskell with refinement
types~\citep{liquidhaskell-dissertation} to enable formal verification, and it
has been applied to cost analysis~\citep{liquidate}. The major difference is
that our work does not require an explicit notion of laziness, as discussed
earlier in this section. Furthermore, \citet{liquidate} verify Haskell programs
written explicitly in the tick monad; to analyze arbitrary Haskell programs,
some monadic translation is necessary.

\paragraph{Nondeterminism and Dual Logics}

Our optimistic and pessimistic specifications are examples of predicate
transformer semantics. They date back to \citet{dijkstra1975}, forming the
basis of much work on the verification of effectful programs in type
Our predicate transformer semantics are two conventional effect
observations~\cite{maillard2019} from the clairvoyance monad---a variant of the
powerset monad---to the specification monads respectively for angelic and
demonic nondeterminism.

The duality between \pessim{} and \optim{} specifications is also the duality of Hoare
logic~\citep{hoare-logic} and reverse Hoare
logic~\cite{rev-hoare,incorrectness}.  Those logics use sets of states to
approximate program behavior.  In Hoare logic, the postcondition
over-approximates the set of reachable states; in reverse Hoare logic, the
postcondition under-approximates the set of reachable states.
Here, we show that abstractions for angelic and demonic nondeterminism
give rise, rather simply, to logics of over- and under-approximations
of time consumption.
The notion of approximation underlying our logics is formally defined as
follows: a set of cost-value pairs $A$ underapproximates a set of pairs $B$ if,
for every $(v,c) ∈A$, there exists $(w,d) ∈B$ which ``costs less and is
more defined'', \ie such that $d ≤c$ and $v ≤w$.
Thus, sets of states are ordered by inclusion in Hoare logic, whereas sets of
cost-value pairs follow a more elaborate order structure in our dual logic,
based on the view that those pairs themselves are approximations of the actual
behavior of lazy programs.

\section{Conclusion and future work}\label{sec:conclusion}

In this paper, we present a novel and simple framework for formally reasoning
about costs of lazy functional programs. The framework is based on a new model
of lazy evaluation: clairvoyant call-by-value~\citep{clairvoyant}, which makes
use of nondeterminism to avoid modeling mutable higher-order state in classic
models of laziness~\citep{launchbury1993}.

Our framework includes a simple clairvoyance monad and a translation from a
typed calculus to programs in this monad that captures the semantics of
clairvoyant call-by-value. Compared with the denotational semantics
of \citeauthor{clairvoyant}, our translation deals with typed programs, does not
rely on domain theory, and accounts for the cost of every nondeterministic
We also develop dual logics \emph{over-} and \emph{under-approximations} similar to
those of \citet{hoare-logic,rev-hoare,incorrectness} that enable local and
modular formal reasoning of computation costs. We show the effectiveness of our
approach via several small case studies.

In future work, we would like to apply this methodology to existing programs
written in Haskell. In particular, we would like to augment tools
like \hstocoq~\citep{hs-to-coq} so that they can automatically translate Haskell
programs to the clairvoyance monad and explore techniques in Coq that can be
used to automate reasoning in those logics.

\begin{acks}

We thank Koen Claessen, who recommended to one author the work
of \citet{clairvoyant} during ICFP'20, and Deepak Garg, who recommended to
another author the work of \citet{danielsson-08} during POPL'21. We thank the
anonymous reviewers of ICFP'21, whose feedback helped improve the paper. We also
thank our shepherd Leonidas Lampropoulos.

This material is based upon work supported by
the \grantsponsor{GS100000001}{National Science
Foundation}{http://dx.doi.org/10.13039/100000001} under Grant
No.~\grantnum{GS100000001}{1521539}, and Grant
No.~\grantnum{GS100000001}{2006535}.  Any opinions, findings, and conclusions or
recommendations expressed in this material are those of the authors and do not
necessarily reflect the views of the National Science Foundation.
\end{acks}

%%% -*-BibTeX-*-
%%% Do NOT edit. File created by BibTeX with style
%%% ACM-Reference-Format-Journals [18-Jan-2012].

\begin{thebibliography}{51}

%%% ====================================================================
%%% NOTE TO THE USER: you can override these defaults by providing
%%% customized versions of any of these macros before the \bibliography
%%% command.  Each of them MUST provide its own final punctuation,
%%% except for \shownote{}, \showDOI{}, and \showURL{}.  The latter two
%%% do not use final punctuation, in order to avoid confusing it with
%%% the Web address.
%%% To suppress output of a particular field, define its macro to expand
%%% to an empty string, or better, \unskip, like this:
%%% \newcommand{\showDOI}[1]{\unskip}   % LaTeX syntax
%%% \def \showDOI #1{\unskip}           % plain TeX syntax
%%% ====================================================================

\ifx \showCODEN    \undefined \def \showCODEN     #1{\unskip}     \fi
\ifx \showDOI      \undefined \def \showDOI       #1{#1}\fi
\ifx \showISBNx    \undefined \def \showISBNx     #1{\unskip}     \fi
\ifx \showISBNxiii \undefined \def \showISBNxiii  #1{\unskip}     \fi
\ifx \showISSN     \undefined \def \showISSN      #1{\unskip}     \fi
\ifx \showLCCN     \undefined \def \showLCCN      #1{\unskip}     \fi
\ifx \shownote     \undefined \def \shownote      #1{#1}          \fi
\ifx \showarticletitle \undefined \def \showarticletitle #1{#1}   \fi
\ifx \showURL      \undefined \def \showURL       {\relax}        \fi
% The following commands are used for tagged output and should be
% invisible to TeX
\providecommand\bibfield[2]{#2}
\providecommand\bibinfo[2]{#2}
\providecommand\natexlab[1]{#1}
\providecommand\showeprint[2][]{arXiv:#2}

\bibitem[\protect\citeauthoryear{Abel, Benke, Bove, Hughes, and Norell}{Abel
\bibfield{author}{\bibinfo{person}{Andreas Abel}, \bibinfo{person}{Marcin
Benke}, \bibinfo{person}{Ana Bove}, \bibinfo{person}{John Hughes}, {and}
\bibinfo{person}{Ulf Norell}.} \bibinfo{year}{2005}\natexlab{}.
\newblock \showarticletitle{Verifying Haskell programs using constructive type
theory}. In \bibinfo{booktitle}{\emph{Proceedings of the {ACM} {SIGPLAN}
Workshop on Haskell, Haskell 2005, Tallinn, Estonia, September 30, 2005}},
\bibfield{editor}{\bibinfo{person}{Daan Leijen}} (Ed.).
\bibinfo{publisher}{{ACM}}, \bibinfo{pages}{62--73}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/1088348.1088355}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Breitner, Spector{-}Zabusky, Li, Rizkallah,
Wiegley, Cohen, and Weirich}{Breitner et~al\mbox{.}}{2021}]%
\bibfield{author}{\bibinfo{person}{Joachim Breitner}, \bibinfo{person}{Antal
Spector{-}Zabusky}, \bibinfo{person}{Yao Li}, \bibinfo{person}{Christine
Rizkallah}, \bibinfo{person}{John Wiegley}, \bibinfo{person}{Joshua Cohen},
{and} \bibinfo{person}{Stephanie Weirich}.} \bibinfo{year}{2021}\natexlab{}.
\newblock \showarticletitle{Ready, Set, Verify! Applying hs-to-coq to
real-world Haskell code}.
\newblock \bibinfo{journal}{\emph{Journal of Functional Programming}}
\bibinfo{volume}{31} (\bibinfo{year}{2021}), \bibinfo{pages}{e5}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1017/S0956796820000283}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Chargu{\'{e}}raud and
Pottier}{Chargu{\'{e}}raud and Pottier}{2019}]%
\bibfield{author}{\bibinfo{person}{Arthur Chargu{\'{e}}raud} {and}
\bibinfo{person}{Fran{\c{c}}ois Pottier}.} \bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{Verifying the Correctness and Amortized Complexity
of a Union-Find Implementation in Separation Logic with Time Credits}.
\newblock \bibinfo{journal}{\emph{J. Autom. Reason.}} \bibinfo{volume}{62},
\bibinfo{number}{3} (\bibinfo{year}{2019}), \bibinfo{pages}{331--365}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/s10817-017-9431-7}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Christiansen}{Christiansen}{2011}]%
\bibfield{author}{\bibinfo{person}{Jan Christiansen}.}
\bibinfo{year}{2011}\natexlab{}.
\newblock \showarticletitle{Sloth - {A} Tool for Checking Minimal-Strictness}.
In \bibinfo{booktitle}{\emph{Practical Aspects of Declarative Languages -
13th International Symposium, {PADL} 2011, Austin, TX, USA, January 24-25,
2011. Proceedings}} \emph{(\bibinfo{series}{Lecture Notes in Computer
Science})}, \bibfield{editor}{\bibinfo{person}{Ricardo Rocha} {and}
\bibinfo{person}{John Launchbury}} (Eds.), Vol.~\bibinfo{volume}{6539}.
\bibinfo{publisher}{Springer}, \bibinfo{pages}{160--174}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-642-18378-2\_14}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Christiansen and Seidel}{Christiansen and
\bibfield{author}{\bibinfo{person}{Jan Christiansen} {and}
\bibinfo{person}{Daniel Seidel}.} \bibinfo{year}{2011}\natexlab{}.
\newblock \showarticletitle{Minimally strict polymorphic functions}. In
\bibinfo{booktitle}{\emph{Proceedings of the 13th International {ACM}
{SIGPLAN} Conference on Principles and Practice of Declarative Programming,
July 20-22, 2011, Odense, Denmark}}, \bibfield{editor}{\bibinfo{person}{Peter
Schneider{-}Kamp} {and} \bibinfo{person}{Michael Hanus}} (Eds.).
\bibinfo{publisher}{{ACM}}, \bibinfo{pages}{53--64}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/2003476.2003487}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Crary and Weirich}{Crary and Weirich}{2000}]%
\bibfield{author}{\bibinfo{person}{Karl Crary} {and} \bibinfo{person}{Stephanie
Weirich}.} \bibinfo{year}{2000}\natexlab{}.
\newblock \showarticletitle{Resource Bound Certification}. In
\bibinfo{booktitle}{\emph{{POPL} 2000, Proceedings of the 27th {ACM}
{SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, Boston,
Massachusetts, USA, January 19-21, 2000}},
\bibfield{editor}{\bibinfo{person}{Mark~N. Wegman} {and}
\bibinfo{person}{Thomas~W. Reps}} (Eds.). \bibinfo{publisher}{{ACM}},
\bibinfo{pages}{184--198}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/325694.325716}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Cutler, Licata, and Danner}{Cutler
\bibfield{author}{\bibinfo{person}{Joseph~W. Cutler},
\bibinfo{person}{Daniel~R. Licata}, {and} \bibinfo{person}{Norman Danner}.}
\bibinfo{year}{2020}\natexlab{}.
\newblock \showarticletitle{Denotational recurrence extraction for amortized
\newblock \bibinfo{journal}{\emph{Proc. {ACM} Program. Lang.}}
\bibinfo{volume}{4}, \bibinfo{number}{{ICFP}} (\bibinfo{year}{2020}),
\bibinfo{pages}{97:1--97:29}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/3408979}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Danielsson}{Danielsson}{2008}]%
\bibfield{author}{\bibinfo{person}{Nils~Anders Danielsson}.}
\bibinfo{year}{2008}\natexlab{}.
\newblock \showarticletitle{Lightweight semiformal time complexity analysis for
purely functional data structures}. In \bibinfo{booktitle}{\emph{Proceedings
of the 35th {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming
Languages, {POPL} 2008, San Francisco, California, USA, January 7-12, 2008}},
\bibfield{editor}{\bibinfo{person}{George~C. Necula} {and}
\bibinfo{person}{Philip Wadler}} (Eds.). \bibinfo{publisher}{{ACM}},
\bibinfo{pages}{133--144}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/1328438.1328457}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{de~Vries and Koutavas}{de~Vries and
\bibfield{author}{\bibinfo{person}{Edsko de Vries} {and}
\bibinfo{person}{Vasileios Koutavas}.} \bibinfo{year}{2011}\natexlab{}.
\newblock \showarticletitle{Reverse Hoare Logic}. In
\bibinfo{booktitle}{\emph{Software Engineering and Formal Methods - 9th
International Conference, {SEFM} 2011, Montevideo, Uruguay, November 14-18,
2011. Proceedings}} \emph{(\bibinfo{series}{Lecture Notes in Computer
Science})}, \bibfield{editor}{\bibinfo{person}{Gilles Barthe},
\bibinfo{person}{Alberto Pardo}, {and} \bibinfo{person}{Gerardo Schneider}}
(Eds.), Vol.~\bibinfo{volume}{7041}. \bibinfo{publisher}{Springer},
\bibinfo{pages}{155--171}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-642-24690-6\_12}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Dijkstra}{Dijkstra}{1975}]%
\bibfield{author}{\bibinfo{person}{Edsger~W. Dijkstra}.}
\bibinfo{year}{1975}\natexlab{}.
\newblock \showarticletitle{Guarded Commands, Nondeterminacy and Formal
Derivation of Programs}.
\newblock \bibinfo{journal}{\emph{Commun. {ACM}}} \bibinfo{volume}{18},
\bibinfo{number}{8} (\bibinfo{year}{1975}), \bibinfo{pages}{453--457}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/360933.360975}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Dylus, Christiansen, and Teegen}{Dylus
\bibfield{author}{\bibinfo{person}{Sandra Dylus}, \bibinfo{person}{Jan
Christiansen}, {and} \bibinfo{person}{Finn Teegen}.}
\bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{One Monad to Prove Them All}.
\newblock \bibinfo{journal}{\emph{Art Sci. Eng. Program.}} \bibinfo{volume}{3},
\bibinfo{number}{3} (\bibinfo{year}{2019}), \bibinfo{pages}{8}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.22152/programming-journal.org/2019/3/8}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Eberl}{Eberl}{2021}]%
\bibfield{author}{\bibinfo{person}{Manuel Eberl}.}
\bibinfo{year}{2021}\natexlab{}.
\newblock \emph{\bibinfo{title}{Asymptotic Reasoning in a Proof Assistant}}.
\newblock Dissertation. \bibinfo{school}{Technical University of Munich,
Munich, Germany}.
\newblock
\urldef\tempurl%
\url{http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20210121-1554821-1-2}
\showURL{%
\tempurl}

\bibitem[\protect\citeauthoryear{Foner, Zhang, and Lampropoulos}{Foner
\bibfield{author}{\bibinfo{person}{Kenneth Foner}, \bibinfo{person}{Hengchu
Zhang}, {and} \bibinfo{person}{Leonidas Lampropoulos}.}
\bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{Keep your laziness in check}.
\newblock \bibinfo{journal}{\emph{Proc. {ACM} Program. Lang.}}
\bibinfo{volume}{2}, \bibinfo{number}{{ICFP}} (\bibinfo{year}{2018}),
\bibinfo{pages}{102:1--102:30}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/3236797}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Friedman and Wise}{Friedman and Wise}{1974}]%
\bibfield{author}{\bibinfo{person}{Daniel~P. Friedman} {and}
\bibinfo{person}{David~S. Wise}.} \bibinfo{year}{1974}\natexlab{}.
\newblock \bibinfo{booktitle}{\emph{Unwinding Structured Recursions into
\newblock \bibinfo{type}{Technical Report} TR19. \bibinfo{institution}{Indiana
\newblock
\urldef\tempurl%
\url{https://help.luddy.indiana.edu/techreports/TRNNN.cgi?trnum=TR19}
\showURL{%
\tempurl}

\bibitem[\protect\citeauthoryear{Gu{\'{e}}neau}{Gu{\'{e}}neau}{2019}]%
\bibfield{author}{\bibinfo{person}{Arma{\"{e}}l Gu{\'{e}}neau}.}
\bibinfo{year}{2019}\natexlab{}.
\newblock \emph{\bibinfo{title}{Mechanized Verification of the Correctness and
Asymptotic Complexity of Programs. (V{\'{e}}rification m{\'{e}}canis{\'{e}}e
de la correction et complexit{\'{e}} asymptotique de programmes)}}.
\newblock \bibinfo{thesistype}{Ph.D. Dissertation}. \bibinfo{school}{Inria,
Paris, France}.
\newblock
\urldef\tempurl%
\url{https://tel.archives-ouvertes.fr/tel-02437532}
\showURL{%
\tempurl}

\bibitem[\protect\citeauthoryear{Gu{\'{e}}neau, Chargu{\'{e}}raud, and
Pottier}{Gu{\'{e}}neau et~al\mbox{.}}{2018}]%
\bibfield{author}{\bibinfo{person}{Arma{\"{e}}l Gu{\'{e}}neau},
\bibinfo{person}{Arthur Chargu{\'{e}}raud}, {and}
\bibinfo{person}{Fran{\c{c}}ois Pottier}.} \bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{A Fistful of Dollars: Formalizing Asymptotic
Complexity Claims via Deductive Program Verification}. In
\bibinfo{booktitle}{\emph{Programming Languages and Systems - 27th European
Symposium on Programming, {ESOP} 2018, Held as Part of the European Joint
Conferences on Theory and Practice of Software, {ETAPS} 2018, Thessaloniki,
Greece, April 14-20, 2018, Proceedings}} \emph{(\bibinfo{series}{Lecture
Notes in Computer Science})}, \bibfield{editor}{\bibinfo{person}{Amal Ahmed}}
(Ed.), Vol.~\bibinfo{volume}{10801}. \bibinfo{publisher}{Springer},
\bibinfo{pages}{533--560}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-319-89884-1_19}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Hackett and Hutton}{Hackett and
\bibfield{author}{\bibinfo{person}{Jennifer Hackett} {and}
\bibinfo{person}{Graham Hutton}.} \bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{Call-by-need is clairvoyant call-by-value}.
\newblock \bibinfo{journal}{\emph{Proc. {ACM} Program. Lang.}}
\bibinfo{volume}{3}, \bibinfo{number}{{ICFP}} (\bibinfo{year}{2019}),
\bibinfo{pages}{114:1--114:23}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/3341718}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Handley, Vazou, and Hutton}{Handley
\bibfield{author}{\bibinfo{person}{Martin A.~T. Handley}, \bibinfo{person}{Niki
Vazou}, {and} \bibinfo{person}{Graham Hutton}.}
\bibinfo{year}{2020}\natexlab{}.
\newblock \showarticletitle{Liquidate your assets: reasoning about resource
usage in Liquid Haskell}.
\newblock \bibinfo{journal}{\emph{Proc. {ACM} Program. Lang.}}
\bibinfo{volume}{4}, \bibinfo{number}{{POPL}} (\bibinfo{year}{2020}),
\bibinfo{pages}{24:1--24:27}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/3371092}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Henderson and Morris}{Henderson and
\bibfield{author}{\bibinfo{person}{Peter Henderson} {and}
\bibinfo{person}{James~H. Morris, Jr.}} \bibinfo{year}{1976}\natexlab{}.
\newblock \showarticletitle{A Lazy Evaluator}. In
\bibinfo{booktitle}{\emph{Conference Record of the Third {ACM} Symposium on
Principles of Programming Languages, Atlanta, Georgia, USA, January 1976}},
\bibfield{editor}{\bibinfo{person}{Susan~L. Graham},
\bibinfo{person}{Robert~M. Graham}, \bibinfo{person}{Michael~A. Harrison},
\bibinfo{person}{William~I. Grosky}, {and} \bibinfo{person}{Jeffrey~D.
Ullman}} (Eds.). \bibinfo{publisher}{{ACM} Press}, \bibinfo{pages}{95--103}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/800168.811543}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Hoare}{Hoare}{1969}]%
\bibfield{author}{\bibinfo{person}{C.~A.~R. Hoare}.}
\bibinfo{year}{1969}\natexlab{}.
\newblock \showarticletitle{An Axiomatic Basis for Computer Programming}.
\newblock \bibinfo{journal}{\emph{Commun. {ACM}}} \bibinfo{volume}{12},
\bibinfo{number}{10} (\bibinfo{year}{1969}), \bibinfo{pages}{576--580}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/363235.363259}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Hoffmann, Aehlig, and Hofmann}{Hoffmann
\bibfield{author}{\bibinfo{person}{Jan Hoffmann}, \bibinfo{person}{Klaus
Aehlig}, {and} \bibinfo{person}{Martin Hofmann}.}
\bibinfo{year}{2012}\natexlab{}.
\newblock \showarticletitle{Multivariate amortized resource analysis}.
\newblock \bibinfo{journal}{\emph{{ACM} Trans. Program. Lang. Syst.}}
\bibinfo{volume}{34}, \bibinfo{number}{3} (\bibinfo{year}{2012}),
\bibinfo{pages}{14:1--14:62}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/2362389.2362393}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Hughes}{Hughes}{1986}]%
\bibfield{author}{\bibinfo{person}{John Hughes}.}
\bibinfo{year}{1986}\natexlab{}.
\newblock \showarticletitle{A Novel Representation of Lists and its Application
to the Function "reverse"}.
\newblock \bibinfo{journal}{\emph{Inf. Process. Lett.}} \bibinfo{volume}{22},
\bibinfo{number}{3} (\bibinfo{year}{1986}), \bibinfo{pages}{141--144}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1016/0020-0190(86)90059-1}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Hughes}{Hughes}{1989}]%
\bibfield{author}{\bibinfo{person}{John Hughes}.}
\bibinfo{year}{1989}\natexlab{}.
\newblock \showarticletitle{Why Functional Programming Matters}.
\newblock \bibinfo{journal}{\emph{Comput. J.}} \bibinfo{volume}{32},
\bibinfo{number}{2} (\bibinfo{year}{1989}), \bibinfo{pages}{98--107}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1093/comjnl/32.2.98}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Josephs}{Josephs}{1989}]%
\bibfield{author}{\bibinfo{person}{Mark~B. Josephs}.}
\bibinfo{year}{1989}\natexlab{}.
\newblock \showarticletitle{The Semantics of Lazy Functional Languages}.
\newblock \bibinfo{journal}{\emph{Theor. Comput. Sci.}} \bibinfo{volume}{68},
\bibinfo{number}{1} (\bibinfo{year}{1989}), \bibinfo{pages}{105--111}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1016/0304-3975(89)90122-9}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Lago}{Lago}{2011}]%
\bibfield{author}{\bibinfo{person}{Ugo~Dal Lago}.}
\bibinfo{year}{2011}\natexlab{}.
\newblock \showarticletitle{A Short Introduction to Implicit Computational
Complexity}. In \bibinfo{booktitle}{\emph{Lectures on Logic and Computation -
{ESSLLI} 2010 Copenhagen, Denmark, August 2010, {ESSLLI} 2011, Ljubljana,
Slovenia, August 2011, Selected Lecture Notes}}
\emph{(\bibinfo{series}{Lecture Notes in Computer Science})},
\bibfield{editor}{\bibinfo{person}{Nick Bezhanishvili} {and}
\bibinfo{person}{Valentin Goranko}} (Eds.), Vol.~\bibinfo{volume}{7388}.
\bibinfo{publisher}{Springer}, \bibinfo{pages}{89--109}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-642-31485-8\_3}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Launchbury}{Launchbury}{1993}]%
\bibfield{author}{\bibinfo{person}{John Launchbury}.}
\bibinfo{year}{1993}\natexlab{}.
\newblock \showarticletitle{A Natural Semantics for Lazy Evaluation}. In
\bibinfo{booktitle}{\emph{Conference Record of the Twentieth Annual {ACM}
{SIGPLAN-SIGACT} Symposium on Principles of Programming Languages,
Charleston, South Carolina, USA, January 1993}},
\bibfield{editor}{\bibinfo{person}{Mary S.~Van Deusen} {and}
\bibinfo{person}{Bernard Lang}} (Eds.). \bibinfo{publisher}{{ACM} Press},
\bibinfo{pages}{144--154}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/158511.158618}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Li, Xia, and Weirich}{Li
\bibfield{author}{\bibinfo{person}{Yao Li}, \bibinfo{person}{Li{-}yao Xia},
{and} \bibinfo{person}{Stephanie Weirich}.} \bibinfo{year}{2021}\natexlab{}.
\newblock \bibinfo{title}{Reasoning about the garden of forking paths
\newblock
\newblock
\urldef\tempurl%
\url{https://doi.org/10.5281/zenodo.4771438}
\showDOI{\tempurl}
\newblock
\shownote{GitHub repository at:
\url{https://github.com/lastland/ClairvoyanceMonad}.}

\bibitem[\protect\citeauthoryear{Liang, Hudak, and Jones}{Liang
\bibfield{author}{\bibinfo{person}{Sheng Liang}, \bibinfo{person}{Paul Hudak},
{and} \bibinfo{person}{Mark~P. Jones}.} \bibinfo{year}{1995}\natexlab{}.
\newblock \showarticletitle{Monad Transformers and Modular Interpreters}. In
\bibinfo{booktitle}{\emph{Conference Record of POPL'95: 22nd {ACM}
{SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, San
Francisco, California, USA, January 23-25, 1995}},
\bibfield{editor}{\bibinfo{person}{Ron~K. Cytron} {and}
\bibinfo{person}{Peter Lee}} (Eds.). \bibinfo{publisher}{{ACM} Press},
\bibinfo{pages}{333--343}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/199448.199528}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Madhavan, Kulal, and Kuncak}{Madhavan
\bibfield{author}{\bibinfo{person}{Ravichandhran Madhavan},
\bibinfo{person}{Sumith Kulal}, {and} \bibinfo{person}{Viktor Kuncak}.}
\bibinfo{year}{2017}\natexlab{}.
\newblock \showarticletitle{Contract-based resource verification for
higher-order functions with memoization}. In
\bibinfo{booktitle}{\emph{Proceedings of the 44th {ACM} {SIGPLAN} Symposium
on Principles of Programming Languages, {POPL} 2017, Paris, France, January
18-20, 2017}}, \bibfield{editor}{\bibinfo{person}{Giuseppe Castagna} {and}
\bibinfo{person}{Andrew~D. Gordon}} (Eds.). \bibinfo{publisher}{{ACM}},
\bibinfo{pages}{330--343}.
\newblock
\urldef\tempurl%
\url{http://dl.acm.org/citation.cfm?id=3009874}
\showURL{%
\tempurl}

\bibitem[\protect\citeauthoryear{Maillard, Ahman, Atkey, Mart{\'{\i}}nez,
Hritcu, Rivas, and Tanter}{Maillard et~al\mbox{.}}{2019}]%
\bibfield{author}{\bibinfo{person}{Kenji Maillard}, \bibinfo{person}{Danel
Ahman}, \bibinfo{person}{Robert Atkey}, \bibinfo{person}{Guido
Mart{\'{\i}}nez}, \bibinfo{person}{Catalin Hritcu}, \bibinfo{person}{Exequiel
Rivas}, {and} \bibinfo{person}{{\'{E}}ric Tanter}.}
\bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{Dijkstra monads for all}.
\newblock \bibinfo{journal}{\emph{Proc. {ACM} Program. Lang.}}
\bibinfo{volume}{3}, \bibinfo{number}{{ICFP}} (\bibinfo{year}{2019}),
\bibinfo{pages}{104:1--104:29}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/3341708}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Maraist, Odersky, Turner, and Wadler}{Maraist
\bibfield{author}{\bibinfo{person}{John Maraist}, \bibinfo{person}{Martin
Odersky}, \bibinfo{person}{David~N. Turner}, {and} \bibinfo{person}{Philip
Wadler}.} \bibinfo{year}{1995}\natexlab{}.
\newblock \showarticletitle{Call-by-name, call-by-value, call-by-need and the
linear lambda calculus}. In \bibinfo{booktitle}{\emph{Eleventh Annual
Conference on Mathematical Foundations of Programming Semantics, {MFPS} 1995,
Tulane University, New Orleans, LA, USA, March 29 - April 1, 1995}}
\emph{(\bibinfo{series}{Electronic Notes in Theoretical Computer Science})},
\bibfield{editor}{\bibinfo{person}{Stephen~D. Brookes},
\bibinfo{person}{Michael~G. Main}, \bibinfo{person}{Austin Melton}, {and}
\bibinfo{person}{Michael~W. Mislove}} (Eds.), Vol.~\bibinfo{volume}{1}.
\bibinfo{publisher}{Elsevier}, \bibinfo{pages}{370--392}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1016/S1571-0661(04)00022-2}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{\mbox{Coq development team}}{\mbox{Coq
development team}}{2021}]%
\bibfield{author}{\bibinfo{person}{\mbox{Coq development team}}.}
\bibinfo{year}{2021}\natexlab{}.
\newblock \bibinfo{booktitle}{\emph{The Coq proof assistant}}.
\newblock
\urldef\tempurl%
\url{http://coq.inria.fr}
\showURL{%
\tempurl}
\newblock
\shownote{Version 8.13.2.}

\bibitem[\protect\citeauthoryear{Moggi}{Moggi}{1991}]%
\bibfield{author}{\bibinfo{person}{Eugenio Moggi}.}
\bibinfo{year}{1991}\natexlab{}.
\newblock \showarticletitle{Notions of Computation and Monads}.
\newblock \bibinfo{journal}{\emph{Inf. Comput.}} \bibinfo{volume}{93},
\bibinfo{number}{1} (\bibinfo{year}{1991}), \bibinfo{pages}{55--92}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1016/0890-5401(91)90052-4}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Moran and Sands}{Moran and Sands}{1999}]%
\bibfield{author}{\bibinfo{person}{Andrew Moran} {and} \bibinfo{person}{David
Sands}.} \bibinfo{year}{1999}\natexlab{}.
\newblock \showarticletitle{Improvement in a Lazy Context: An Operational
Theory for Call-by-Need}. In \bibinfo{booktitle}{\emph{{POPL} '99,
Proceedings of the 26th {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
Programming Languages, San Antonio, TX, USA, January 20-22, 1999}},
\bibfield{editor}{\bibinfo{person}{Andrew~W. Appel} {and}
\bibinfo{person}{Alex Aiken}} (Eds.). \bibinfo{publisher}{{ACM}},
\bibinfo{pages}{43--56}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/292540.292547}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Nanevski, Morrisett, and Birkedal}{Nanevski
\bibfield{author}{\bibinfo{person}{Aleksandar Nanevski},
\bibinfo{person}{J.~Gregory Morrisett}, {and} \bibinfo{person}{Lars
Birkedal}.} \bibinfo{year}{2008}\natexlab{}.
\newblock \showarticletitle{Hoare type theory, polymorphism and separation}.
\newblock \bibinfo{journal}{\emph{J. Funct. Program.}} \bibinfo{volume}{18},
\bibinfo{number}{5-6} (\bibinfo{year}{2008}), \bibinfo{pages}{865--911}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1017/S0956796808006953}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{O'Hearn}{O'Hearn}{2020}]%
\bibfield{author}{\bibinfo{person}{Peter~W. O'Hearn}.}
\bibinfo{year}{2020}\natexlab{}.
\newblock \showarticletitle{Incorrectness logic}.
\newblock \bibinfo{journal}{\emph{Proc. {ACM} Program. Lang.}}
\bibinfo{volume}{4}, \bibinfo{number}{{POPL}} (\bibinfo{year}{2020}),
\bibinfo{pages}{10:1--10:32}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/3371078}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Okasaki}{Okasaki}{1999}]%
\bibfield{author}{\bibinfo{person}{Chris Okasaki}.}
\bibinfo{year}{1999}\natexlab{}.
\newblock \bibinfo{booktitle}{\emph{Purely functional data structures}}.
\newblock \bibinfo{publisher}{Cambridge University Press}.
\newblock
\showISBNx{978-0-521-66350-2}

\bibitem[\protect\citeauthoryear{Petricek}{Petricek}{2012}]%
\bibfield{author}{\bibinfo{person}{Tomas Petricek}.}
\bibinfo{year}{2012}\natexlab{}.
\newblock \showarticletitle{Evaluation strategies for monadic computations}. In
\bibinfo{booktitle}{\emph{Proceedings Fourth Workshop on Mathematically
Structured Functional Programming, MSFP@ETAPS 2012, Tallinn, Estonia, 25
March 2012}} \emph{(\bibinfo{series}{{EPTCS}})},
\bibfield{editor}{\bibinfo{person}{James Chapman} {and}
\bibinfo{person}{Paul~Blain Levy}} (Eds.), Vol.~\bibinfo{volume}{76}.
\bibinfo{pages}{68--89}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.4204/EPTCS.76.7}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Rajani, Gaboardi, Garg, and Hoffmann}{Rajani
\bibfield{author}{\bibinfo{person}{Vineet Rajani}, \bibinfo{person}{Marco
Gaboardi}, \bibinfo{person}{Deepak Garg}, {and} \bibinfo{person}{Jan
Hoffmann}.} \bibinfo{year}{2021}\natexlab{}.
\newblock \showarticletitle{A unifying type-theory for higher-order (amortized)
cost analysis}.
\newblock \bibinfo{journal}{\emph{Proc. {ACM} Program. Lang.}}
\bibinfo{volume}{5}, \bibinfo{number}{{POPL}} (\bibinfo{year}{2021}),
\bibinfo{pages}{1--28}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/3434308}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Sabry and Felleisen}{Sabry and
\bibfield{author}{\bibinfo{person}{Amr Sabry} {and} \bibinfo{person}{Matthias
Felleisen}.} \bibinfo{year}{1992}\natexlab{}.
\newblock \showarticletitle{Reasoning About Programs in Continuation-Passing
Style}. In \bibinfo{booktitle}{\emph{Proceedings of the Conference on Lisp
and Functional Programming, {LFP} 1992, San Francisco, California, USA, 22-24
June 1992}}. \bibinfo{publisher}{{ACM}}, \bibinfo{pages}{288--298}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/141471.141563}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Scott}{Scott}{1976}]%
\bibfield{author}{\bibinfo{person}{Dana~S. Scott}.}
\bibinfo{year}{1976}\natexlab{}.
\newblock \showarticletitle{Data Types as Lattices}.
\newblock \bibinfo{journal}{\emph{{SIAM} J. Comput.}} \bibinfo{volume}{5},
\bibinfo{number}{3} (\bibinfo{year}{1976}), \bibinfo{pages}{522--587}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1137/0205037}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Spector{-}Zabusky, Breitner, Li, and
Weirich}{Spector{-}Zabusky et~al\mbox{.}}{2019}]%
\bibfield{author}{\bibinfo{person}{Antal Spector{-}Zabusky},
\bibinfo{person}{Joachim Breitner}, \bibinfo{person}{Yao Li}, {and}
\bibinfo{person}{Stephanie Weirich}.} \bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{Embracing a mechanized formalization gap}.
\newblock \bibinfo{journal}{\emph{CoRR}}  \bibinfo{volume}{abs/1910.11724}
\newblock
\showeprint[arxiv]{1910.11724}
\urldef\tempurl%
\url{http://arxiv.org/abs/1910.11724}
\showURL{%
\tempurl}

\bibitem[\protect\citeauthoryear{Spector{-}Zabusky, Breitner, Rizkallah, and
Weirich}{Spector{-}Zabusky et~al\mbox{.}}{2018}]%
\bibfield{author}{\bibinfo{person}{Antal Spector{-}Zabusky},
\bibinfo{person}{Joachim Breitner}, \bibinfo{person}{Christine Rizkallah},
{and} \bibinfo{person}{Stephanie Weirich}.} \bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{Total {Haskell} is reasonable {Coq}}. In
\bibinfo{booktitle}{\emph{Proceedings of the 7th {ACM} {SIGPLAN}
International Conference on Certified Programs and Proofs, {CPP} 2018, Los
Angeles, CA, USA, January 8-9, 2018}},
\bibfield{editor}{\bibinfo{person}{June Andronick} {and}
\bibinfo{person}{Amy~P. Felty}} (Eds.). \bibinfo{publisher}{{ACM}},
\bibinfo{pages}{14--27}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/3167092}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Swamy, Weinberger, Schlesinger, Chen, and
Livshits}{Swamy et~al\mbox{.}}{2013}]%
\bibfield{author}{\bibinfo{person}{Nikhil Swamy}, \bibinfo{person}{Joel
Weinberger}, \bibinfo{person}{Cole Schlesinger}, \bibinfo{person}{Juan Chen},
{and} \bibinfo{person}{Benjamin Livshits}.} \bibinfo{year}{2013}\natexlab{}.
\newblock \showarticletitle{Verifying higher-order programs with the Dijkstra
monad}. In \bibinfo{booktitle}{\emph{{ACM} {SIGPLAN} Conference on
Programming Language Design and Implementation, {PLDI} '13, Seattle, WA, USA,
June 16-19, 2013}}, \bibfield{editor}{\bibinfo{person}{Hans{-}Juergen Boehm}
{and} \bibinfo{person}{Cormac Flanagan}} (Eds.). \bibinfo{publisher}{{ACM}},
\bibinfo{pages}{387--398}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/2491956.2491978}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Swierstra}{Swierstra}{2009}]%
\bibfield{author}{\bibinfo{person}{Wouter Swierstra}.}
\bibinfo{year}{2009}\natexlab{}.
\newblock \showarticletitle{A Hoare Logic for the State Monad}. In
\bibinfo{booktitle}{\emph{Theorem Proving in Higher Order Logics, 22nd
International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009.
Proceedings}} \emph{(\bibinfo{series}{Lecture Notes in Computer Science})},
\bibfield{editor}{\bibinfo{person}{Stefan Berghofer}, \bibinfo{person}{Tobias
Nipkow}, \bibinfo{person}{Christian Urban}, {and} \bibinfo{person}{Makarius
Wenzel}} (Eds.), Vol.~\bibinfo{volume}{5674}. \bibinfo{publisher}{Springer},
\bibinfo{pages}{440--451}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-642-03359-9\_30}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Swierstra and Baanen}{Swierstra and
\bibfield{author}{\bibinfo{person}{Wouter Swierstra} {and} \bibinfo{person}{Tim
Baanen}.} \bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{A predicate transformer semantics for effects
(functional pearl)}.
\newblock \bibinfo{journal}{\emph{Proc. {ACM} Program. Lang.}}
\bibinfo{volume}{3}, \bibinfo{number}{{ICFP}} (\bibinfo{year}{2019}),
\bibinfo{pages}{103:1--103:26}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/3341707}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Turner}{Turner}{2004}]%
\bibfield{author}{\bibinfo{person}{D.~A. Turner}.}
\bibinfo{year}{2004}\natexlab{}.
\newblock \showarticletitle{Total Functional Programming}.
\newblock \bibinfo{journal}{\emph{J. Univers. Comput. Sci.}}
\bibinfo{volume}{10}, \bibinfo{number}{7} (\bibinfo{year}{2004}),
\bibinfo{pages}{751--768}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.3217/jucs-010-07-0751}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Uustalu}{Uustalu}{2002}]%
\bibfield{author}{\bibinfo{person}{Tarmo Uustalu}.}
\bibinfo{year}{2002}\natexlab{}.
\newblock \showarticletitle{Monad Translating Inductive and Coinductive Types}.
In \bibinfo{booktitle}{\emph{Types for Proofs and Programs, Second
International Workshop, {TYPES} 2002, Berg en Dal, The Netherlands, April
24-28, 2002, Selected Papers}} \emph{(\bibinfo{series}{Lecture Notes in
Computer Science})}, \bibfield{editor}{\bibinfo{person}{Herman Geuvers} {and}
\bibinfo{person}{Freek Wiedijk}} (Eds.), Vol.~\bibinfo{volume}{2646}.
\bibinfo{publisher}{Springer}, \bibinfo{pages}{299--315}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/3-540-39185-1\_17}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Vazou}{Vazou}{2016}]%
\bibfield{author}{\bibinfo{person}{Niki Vazou}.}
\bibinfo{year}{2016}\natexlab{}.
\newblock \emph{\bibinfo{title}{Liquid {Haskell}: {Haskell} as a Theorem
\newblock \bibinfo{thesistype}{Ph.D. Dissertation}. \bibinfo{school}{University
of California, San Diego, {USA}}.
\newblock
\urldef\tempurl%
\url{http://www.escholarship.org/uc/item/8dm057ws}
\showURL{%
\tempurl}

\bibitem[\protect\citeauthoryear{Wadler}{Wadler}{1992}]%
\bibfield{author}{\bibinfo{person}{Philip Wadler}.}
\bibinfo{year}{1992}\natexlab{}.
\newblock \showarticletitle{Comprehending Monads}.
\newblock \bibinfo{journal}{\emph{Math. Struct. Comput. Sci.}}
\bibinfo{volume}{2}, \bibinfo{number}{4} (\bibinfo{year}{1992}),
\bibinfo{pages}{461--493}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1017/S0960129500001560}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Wang, Wang, and Chlipala}{Wang
\bibfield{author}{\bibinfo{person}{Peng Wang}, \bibinfo{person}{Di Wang}, {and}
\bibinfo{person}{Adam Chlipala}.} \bibinfo{year}{2017}\natexlab{}.
\newblock \showarticletitle{{TiML}: a functional language for practical
complexity analysis with invariants}.
\newblock \bibinfo{journal}{\emph{Proc. {ACM} Program. Lang.}}
\bibinfo{volume}{1}, \bibinfo{number}{{OOPSLA}} (\bibinfo{year}{2017}),
\bibinfo{pages}{79:1--79:26}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/3133903}
\showDOI{\tempurl}

\end{thebibliography}

\end{document}