$e:\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}{\mathbb{C}}\times
A$.

###### Proof.

By definition, $e=(c^{\prime},a)$ for some
$c^{\prime}:\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}{\mathbb{C}}$
and $a:A$. Unfolding the definition of $\mathsf{step}$ and free algebra, we
have
$\mathsf{step}^{c}(c^{\prime},a)=(\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}(c)+_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}c^{\prime},a)$,
where
$+_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}$
lifts $+$ using the functorial action of 🌑. Hence it suffices to show
$(\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}(c)+_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}c^{\prime},a)=(c^{\prime},a)$
implies
$\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}{\bot}$.
Suppose
$(\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}(c)+_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}c^{\prime},a)=(c^{\prime},a)$.
By the induction principle of pushouts, there are two cases to consider.
First, suppose
$c^{\prime}=\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}(c^{\prime\prime})$
for some $c^{\prime\prime}:\mathbb{C}$. Because 🌑 is left exact, the equation
$\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}(c)+_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}(c^{\prime\prime})=\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}(c^{\prime\prime})$
is equivalent to
$\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}(c+c^{\prime\prime}=c^{\prime\prime})$.
But we assumed that $c$ is nonzero, so the fact that $\mathbb{C}$ is
cancellative entails $c+c^{\prime\prime}=c^{\prime\prime}\to\bot$, and the
result follows from the functorial action of 🌑. On the other hand, suppose
$c^{\prime}=\ast(u)$ for some $u:\P_{\mathsf{E}}$. By Lemma 5.3, we obtain a
unique proof of
$\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}\bot$.
∎

Because
$\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}\bot=\P_{\mathsf{E}}$,
we know that if $\mathsf{step}$ is degenerate, then the extensional phase
$\P_{\mathsf{E}}$ is derivable. Observing that we placed no restrictions on
the proposition $\P_{\mathsf{E}}$ in the construction of the counting model,
we immediately obtain the desired theorem by instantiating $\P_{\mathsf{E}}$
with the false proposition:

###### Theorem 5.6.

We have that $\nvdash\mathsf{step}^{c}(e)=e$ for any nonzero $c:\mathbb{C}$
and $e:\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}}$.

###  5.3. Validity of extensional cost bounds

We show that extensional inequalities are equivalent to ordinary inequalities
in the ${\textbf{Set}}^{\to}$ model of calf whenever the cost monoid is
_extensional_ in the sense that
$\mathbb{C}\cong\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}{\mathbb{C}}$
and the relation $\leq$ may be characterized using $\Sigma$ and equality
types. As an example, we illustrate the case for the cost monoid $\mathbb{N}$,
noting that the same proof may be easily adapted to other common instances:

###### Theorem 5.7.

We have that
$\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}{(m\leq
n)}$ if and only if $m\leq n$ for all $m,n:\mathbb{\mathbb{N}}$.

###### Proof.

Observe that we may present $m\leq n$ as the type $\Sigma
k:\mathbb{N}.\,n=\mathsf{suc}^{k}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
m$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
m$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
m$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
m$}\mathclose{}{)}}$. By standard results (Rijke et al., 2020) we know that
the property of being extensional is closed under equality and $\Sigma$ types.
Combined with the fact that $\mathbb{N}$ is an extensional type in the
${\textbf{Set}}^{\to}$ model of calf, we conclude that $m\leq n$ is also
extensional, _i.e_. $(m\leq
n)\cong\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}{(m\leq
n)}$. ∎

###### Corollary 5.8.

We have that
$\vdash\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}{(m\leq
n)}$ if and only if $\vdash m\leq n$ for all $m,n:\mathbb{\mathbb{N}}$.

##  6\. Parallelism in calf

Parallelism arises naturally in the setting of calf via an equational
presentation of the profiling semantics of Blelloch and Greiner (1995). Here
we present a version adapted from Harper (2018) in which it is observed that
the source of parallelism can be isolated to the treatment of _pairs_ of
computations: a parallel computation of $A\times B$ is furnished by a new
computation form & that conjoins two independent computations of $A$ and $B$:

$\displaystyle\&$
$\displaystyle:\,\mathrel{\\{A,B:\mathsf{tp}^{+}\\}}\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}})\to\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
B$}\mathclose{}{)}})\to\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A\times B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle A\times
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle A\times
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle A\times
B$}\mathclose{}{)}})$

One may think of a term $e\mathrel{\&}f$ as a computation in which $e$ and $f$
are evaluated simultaneously.

##### Cost structure of parallelism

Blelloch and Greiner (1995) characterize the complexity of a program in terms
of two measures: _work_ , which represents its sequential cost, and _span_ ,
which represents its parallel cost. In calf this structure is recorded by the
_parallel cost monoid_
$\mathbb{C}\coloneqq(\mathbb{N}^{2},\oplus,(0,0),\leq_{\mathbb{N}^{2}})$ in
which $\oplus$ and $\leq_{\mathbb{N}^{2}}$ are component-wise extensions of
addition and $\leq$. Parallel cost composition is then implemented by the
operation
$(w_{1},s_{1})\otimes(w_{2},s_{2})\coloneqq(w_{1}+w_{2},\max{(s_{1},s_{2}}))$
that takes the sum of the works and max of the spans. This provides the
required structure to assemble the cost of a completed parallel pair:

$\displaystyle\&_{\mathsf{join}}$
$\displaystyle:\,\mathrel{\\{A,B,c_{1},c_{2},a,b\\}}\left(\mathsf{step}^{c_{1}}(\mathsf{ret}(a))\right)\mathrel{\&}\left(\mathsf{step}^{c_{2}}(\mathsf{ret}(b))\right)=\mathsf{step}^{c_{1}\otimes
c_{2}}(\mathsf{ret}((a,b)))$

##### Nondegeneracy of parallel calf

Metatheoretic properties of parallel calf follows directly from the counting
model defined in Section 5, given that we can interpret parallel pairing.
Because the new pairing operation is only defined on free algebras, we may use
$\otimes_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}$
(lift of $\otimes$ by the functorial action of 🌑) to define parallel pairing:
$(c_{1},a)\mathrel{\&}(c_{2},b)=(c_{1}\otimes_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}c_{2},(a,b))$.

##### Parallel complexity of sorting

We have verified the sequential and parallel complexity of insertion sort and
merge sort under the comparison cost model. As outlined above, we instantiate
calf with the parallel cost monoid $\mathbb{N}^{2}$ in which the first
component represents the sequential cost and the second component represents
the parallel cost. The analysis is parameterized by a _comparable_ type
$A:\mathsf{tp}^{+}$ that is equipped with a comparison operation
$\leq^{b}:\mathsf{tm}^{+}(A)\to\mathsf{tm}^{+}(A)\to\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathsf{bool}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathsf{bool}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathsf{bool}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathsf{bool}$}\mathclose{}{)}})$.
Consequently, we may enforce the cost model by requiring the comparison
operation $\leq^{b}$ to be uniformly unit cost, _i.e_.
$\mathsf{isBounded}\left(\mathsf{bool};x\leq^{b}y;(1,1)\right)$ for all
$x,y:\mathsf{tm}^{+}(A)$. We have mechanized the following asymptotically
tight cost bounds:

###### Theorem 6.1
(Examples.Sorting.Parallel.InsertionSort.sort≤sort/cost/closed).

For all $l:\mathsf{list}(A)$, we have that
$\mathsf{isBounded}\left(\mathsf{list}(A);\textit{isort}(l);(|l|^{2},|l|^{2})\right)$.

Observe that sequential and parallel complexity coincide for insertion sort
because there is no opportunity for parallelism in the algorithm. The standard
merge sort algorithm enjoys a logarithmic speed up when the recursive calls
are performed in parallel:

###### Theorem 6.2
(Examples.Sorting.Parallel.MergeSort.sort≤sort/cost/closed).

For all $l:\mathsf{list}(A)$, we have that
$\mathsf{isBounded}\left(\mathsf{list}(A);\textit{msort}(l);\left(\left\lceil\log_{2}{|l|}\right\rceil\cdot|l|,2\cdot|l|+\left\lceil\log_{2}{|l|}\right\rceil\right)\right)$.

To obtain a sublinear bound on parallel complexity, one must modify merge sort
to also perform the merging step in parallel, an alteration that slightly
increases the sequential complexity:

###### Theorem 6.3
(Examples.Sorting.Parallel.MergeSortPar.sort≤sort/cost/closed).

For all $l:\mathsf{list}(A)$, we have that
$\mathsf{isBounded}\left(\mathsf{list}(A);\textit{msortPar}(l);\left(\left\lceil\log_{2}{(|l|+1)}\right\rceil^{2}\cdot|l|,\left\lceil\log_{2}{(|l|+1)}\right\rceil^{3}\right)\right)$.

##  7\. Conclusion

Three somewhat contradictory goals guide our type-theoretic approach to cost
analysis:

  1. (1)

Expressiveness: the ability to codify the methods and results of informal
algorithm analysis.

  2. (2)

Certification: programs and their cost bounds should bear their intended
meaning.

  3. (3)

Composition: cost bounds should be composable.

Most extant cost analysis frameworks excel at two out of three of the above.
Type systems defined by intrinsic cost-aware judgments (Hoffmann et al., 2012;
Wang et al., 2017; Rajani et al., 2021) are certified by soundness theorems
and admit composition by construction but lack expressiveness because cost
bounds are often form-constrained and typing derivations cannot exploit
complex behavioral properties. The traditional method for cost accounting
using the writer monad (Handley et al., 2019) provides an expressive and
compositional framework for cost analysis, but this transparent
instrumentation is not certified in the aforementioned sense because programs
in the writer monad do not necessarily accumulate cost faithfully (see Section
1.7.3). Lastly, frameworks for cost analysis in the setting of program logics
(Atkey, 2010; Mével et al., 2019) may be transposed to type theory by working
with a deep embedding of a programming language and its operational semantics
inside type theory. Although this can be developed into an expressive and
certified framework in the sense above, it is not compositional because one
may speak about operational semantics only on closed terms and must quantify
over closing instances for open terms.

In this paper we show that the three goals may be achieved simultaneously.
First, the extensional fragment of calf constituents an ordinary dependent
type theory, which furnished us a rich specification language to formulate two
widely used algorithm analysis techniques and illustrate each through detailed
case studies. Secondly, we see that calf programs account for cost faithfully
because the type of free computations is _abstract_ in the theory, leaving no
opportunity for computations to spuriously abandon accumulated steps or branch
based on the cost component of an input. Lastly, by axiomatizing cost as an
effect in the base CBPV language, we obtain a simple equational theory of cost
that enables compositional cost analysis. We conclude by suggesting two
particularly pertinent directions for future investigations.

##### Automation

In practice the usability of any verification framework may be greatly
improved by automating routine procedures or derivations. In the context of
calf there are two immediate opportunities for automation. On the one hand,
the recurrence extraction step in the method of recurrence relations (as
defined in Section 3.2) may be automated in many cases by incorporating the
mechanism of Kavvos et al. (2019). On the other hand, proofs involving
restricted forms of cost bounds may be automated either by recurrence solving
(_e.g_. the Master theorem) or an automated system such as RaML (Hoffmann et
al., 2012).

##### Full adequacy and partiality

It would be interesting to prove an adequacy result of the form presented in
Kavvos et al. (2019) in which one defines a cost-aware embedding of a source
language (equipped with an operational semantics) in the target language (in
this case calf) and proves that the image of any source program is assigned
the same cost as the cost of the source program that is induced by the
operational semantics. In many cases the source language of interest admits
general recursion; consequently one must arrange for calf to faithfully
interpret non terminating programs. We conjecture that such an adequacy result
may be proved by extending calf with a version of the partiality monad of
Capretta and defining an embedding targeting the monadic fragment.

###### Acknowledgements.

We are grateful to Carlo Angiuli and Alex Kavvos for productive discussions on
the topic of this research, and to Tristan Nguyen at AFOSR for his support.
This work was supported in part by AFOSR under grants MURI FA9550-15-1-0053
and FA9550-19-1-0216, in part by the National Science Foundation under award
number CCF-1901381, and by AFRL through the NDSEG fellowship. 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 AFOSR,
NSF, or AFRL.

## References

  * (1)
  * Acar and Blelloch (2019) Umut A. Acar and Guy E. Blelloch. 2019.  _Algorithms: Parallel and Sequential_.  http:www.algorithms-book.com.
  * Altenkirch and Kaposi (2016a) Thorsten Altenkirch and Ambrus Kaposi. 2016a.  Normalisation by Evaluation for Dependent Types. In _1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 52)_ , Delia Kesner and Brigitte Pientka (Eds.). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 6:1–6:16.  https://doi.org/10.4230/LIPIcs.FSCD.2016.6
  * Altenkirch and Kaposi (2016b) Thorsten Altenkirch and Ambrus Kaposi. 2016b.  Type Theory in Type Theory Using Quotient Inductive Types. In _Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ _(POPL ’16)_. Association for Computing Machinery, St. Petersburg, FL, USA, 18–29.  https://doi.org/10.1145/2837614.2837638
  * Anel and Joyal (2021) Mathieu Anel and André Joyal. 2021.  Topo-logie.  In _New Spaces in Mathematics: Formal and Conceptual Reflections_ , Mathieu Anel and Gabriel Catren (Eds.). Vol. 1. Cambridge University Press, Chapter 4, 155–257.  https://doi.org/10.1017/9781108854429.007
  * Atkey (2010) Robert Atkey. 2010\.  Amortised Resource Analysis with Separation Logic. In _Programming Languages and Systems_ , Andrew D. Gordon (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 85–103.
  * Atkey (2018) Robert Atkey. 2018\.  Syntax and Semantics of Quantitative Type Theory. In _Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science_. Association for Computing Machinery, Oxford, United Kingdom, 56–65.  https://doi.org/10.1145/3209108.3209189
  * Blelloch and Greiner (1995) Guy Blelloch and John Greiner. 1995.  Parallelism in Sequential Functional Languages. In _Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture_. Association for Computing Machinery, La Jolla, California, USA, 226–237.  https://doi.org/10.1145/224164.224210
  * Blelloch and Greiner (1996) Guy E. Blelloch and John Greiner. 1996.  A Provable Time and Space Efficient Implementation of NESL. In _Proceedings of the First ACM SIGPLAN International Conference on Functional Programming_. Association for Computing Machinery, Philadelphia, Pennsylvania, USA, 213–225.  https://doi.org/10.1145/232627.232650
  * Bove and Capretta (2005) Ana Bove and Venanzio Capretta. 2005.  Modelling general recursion in type theory.  _Mathematical Structures in Computer Science_ 15, 4 (2005), 671–708.  https://doi.org/10.1017/S0960129505004822
  * Brady (2013) Edwin Brady. 2013\.  Idris, a general-purpose dependently typed programming language: Design and implementation.  _Journal of Functional Programming_ 23, 5 (Sept. 2013), 552–593.
  * Burton (1982) F. Burton. 1982\.  An Efficient Functional Implementation of FIFO Queues.  _Inf. Process. Lett._ 14 (1982), 205–206.
  * Buzzard et al. (2020) Kevin Buzzard, Johan Commelin, and Patrick Massot. 2020\.  Formalising Perfectoid Spaces. In _Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs_. Association for Computing Machinery, New Orleans, LA, USA, 299–312.  https://doi.org/10.1145/3372885.3373830
  * Capretta (2005) Venanzio Capretta. 2005\.  General Recursion via Coinductive Types.  _Logical Methods in Computer Science_ 1, 2 (2005), 1–18.
  * Chlipala (2013) Adam Chlipala. 2013\.  _Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant_.  The MIT Press.
  * Cockx et al. (2021) Jesper Cockx, Nicolas Tabareau, and Théo Winterhalter. 2021\.  The Taming of the Rew: A Type Theory with Computational Assumptions.  _Proceedings of the ACM on Programming Languages_ (2021).  https://hal.archives-ouvertes.fr/hal-02901011
  * Constable et al. (1986) R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. 1986\.  _Implementing Mathematics with the Nuprl Proof Development System_.  Prentice-Hall, Inc., Upper Saddle River, NJ, USA.
  * Constable and Crary (2002) Robert L. Constable and Karl Crary. 2002.  _Computational complexity and induction for partial computable functions in type theory_.  Cambridge University Press, Cambridge, 164–181.  https://doi.org/10.1017/9781316755983.009
  * Constable and Zlatin (1984) Robert L. Constable and Daniel R. Zlatin. 1984.  The Type Theory of PL/CV3.  _ACM Transactions on Programming Languages and Systems_ 6, 1 (Jan. 1984), 94–117.  https://doi.org/10.1145/357233.357238
  * Coq Development Team (2016) The Coq Development Team. 2016\.  The Coq Proof Assistant Reference Manual.
  * Coquand (2019) Thierry Coquand. 2019\.  Canonicity and normalization for dependent type theory.  _Theoretical Computer Science_ 777 (2019), 184–191.  https://doi.org/10.1016/j.tcs.2019.01.015 arXiv:1810.09367 [cs.PL]  In memory of Maurice Nivat, a founding father of Theoretical Computer Science - Part I.
  * Cormen et al. (2009) Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009.  _Introduction to Algorithms, 3rd Edition_.  MIT Press.  http://mitpress.mit.edu/books/introduction-algorithms
  * Crary and Weirich (2000) Karl Crary and Stephanie Weirich. 2000.  Resource Bound Certification. In _Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_. Association for Computing Machinery, Boston, MA, USA, 184–198.  https://doi.org/10.1145/325694.325716
  * Danner et al. (2015) Norman Danner, Daniel R. Licata, and Ramyaa. 2015.  Denotational cost semantics for functional languages with inductive types. In _Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015_ , Kathleen Fisher and John H. Reppy (Eds.). Association for Computing Machinery, 140–151.  https://doi.org/10.1145/2784731.2784749
  * Davies and Pfenning (1999) Rowan Davies and Frank Pfenning. 1999.  A Modal Analysis of Staged Computation.  _J. ACM_ 48 (Sept. 1999).  https://doi.org/10.1145/382780.382785
  * Eberl (2015) Manuel Eberl. 2015\.  The Akra-Bazzi theorem and the Master theorem.  _Archive of Formal Proofs_ (July 2015).  https://isa-afp.org/entries/Akra_Bazzi.html, Formal proof development.
  * Eberl (2017a) Manuel Eberl. 2017a.  The Median-of-Medians Selection Algorithm.  _Archive of Formal Proofs_ (Dec. 2017).  https://isa-afp.org/entries/Median_Of_Medians_Selection.html, Formal proof development.
  * Eberl (2017b) Manuel Eberl. 2017b.  The number of comparisons in QuickSort.  _Archive of Formal Proofs_ (March 2017).  https://isa-afp.org/entries/Quick_Sort_Cost.html, Formal proof development.
  * Fiore et al. (2021) Marcelo P. Fiore, Andrew M. Pitts, and S. C. Steenkamp. 2021\.  Quotients, inductive types, and quotient inductive types. (2021).  arXiv:2101.02994 [cs.LO]
  * Gonthier (2008) G. Gonthier. 2008\.  Formal Proof — The Four-Color Theorem.  _Notices of the AMS_ 55, 11 (2008).  https://www.ams.org/notices/200811/tx081101382p.pdf
  * Gratzer and Sterling (2020) Daniel Gratzer and Jonathan Sterling. 2020.  Syntactic categories for dependent type theory: sketching and adequacy. (2020).  arXiv:2012.10783 [cs.LO]
  * Greiner and Blelloch (1999) John Greiner and Guy E. Blelloch. 1999.  A Provably Time-Efficient Parallel Implementation of Full Speculation.  _ACM Transactions on Programming Languages and Systems_ 21, 2 (March 1999), 240–285.  https://doi.org/10.1145/316686.316690
  * Gries (1987) David Gries. 1987\.  _The Science of Programming_ (1st ed.).  Springer-Verlag, Berlin, Heidelberg.
  * Han and van Doorn (2020) Jesse Michael Han and Floris van Doorn. 2020.  A Formal Proof of the Independence of the Continuum Hypothesis. In _Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs_. Association for Computing Machinery, New Orleans, LA, USA, 353–366.  https://doi.org/10.1145/3372885.3373826
  * Handley et al. (2019) Martin A. T. Handley, Niki Vazou, and Graham Hutton. 2019\.  Liquidate Your Assets: Reasoning about Resource Usage in Liquid Haskell.  _Proceedings of the ACM on Programming Languages_ 4, POPL (Dec. 2019).  https://doi.org/10.1145/3371092
  * Harper (2018) Robert Harper. 2018\.  PFPL Supplement: Types and Parallelism. (2018).  https://www.cs.cmu.edu/~rwh/pfpl/supplements/par.pdf
  * Harper et al. (1990) Robert Harper, John C. Mitchell, and Eugenio Moggi. 1990\.  Higher-Order Modules and the Phase Distinction. In _Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_. Association for Computing Machinery, San Francisco, California, USA, 341–354.  https://doi.org/10.1145/96709.96744
  * Hoffmann et al. (2012) Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. 2012\.  Resource Aware ML. In _Computer Aided Verification_ , P. Madhusudan and Sanjit A. Seshia (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 781–786.
  * Hofmann (2000) Martin Hofmann. 2000\.  A Type System for Bounded Space and Functional In-Place Update–Extended Abstract. In _Proceedings of the 9th European Symposium on Programming Languages and Systems_. Springer-Verlag, Berlin, Heidelberg, 165–179.
  * Hofmann and Jost (2003) Martin Hofmann and Steffen Jost. 2003.  Static Prediction of Heap Space Usage for First-Order Functional Programs. In _Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_. Association for Computing Machinery, New Orleans, Louisiana, USA, 185–197.  https://doi.org/10.1145/604131.604148
  * Hofmann et al. (2021) Martin Hofmann, Lorenz Leutgeb, Georg Moser, David Obwaller, and Florian Zuleger. 2021.  Type-Based Analysis of Logarithmic Amortised Complexity.  _CoRR_ abs/2101.12029 (2021).  arXiv:2101.12029 https://arxiv.org/abs/2101.12029
  * Hood and Melville (1981) Robert Hood and Robert Melville. 1981.  Real-time queue operations in pure LISP.  _Inform. Process. Lett._ 13, 2 (1981), 50–54.  https://doi.org/10.1016/0020-0190(81)90030-2
  * Jost et al. (2010) Steffen Jost, Kevin Hammond, Hans-Wolfgang Loidl, and Martin Hofmann. 2010.  Static determination of quantitative resource usage for higher-order programs. In _Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010_ , Manuel V. Hermenegildo and Jens Palsberg (Eds.). Association for Computing Machinery, 223–236.  https://doi.org/10.1145/1706299.1706327
  * Jung et al. (2018) Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. 2018.  Iris from the ground up: A modular foundation for higher-order concurrent separation logic.  _Journal of Functional Programming_ 28 (2018), e20.  https://doi.org/10.1017/S0956796818000151
  * Jung et al. (2015) Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015.  Iris: Monoids and Invariants As an Orthogonal Basis for Concurrent Reasoning. In _POPL ’15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_. Association for Computing Machinery, Mumbai, India, 637–650.  https://doi.org/10.1145/2676726.2676980
  * Kahn and Hoffmann (2020) David M. Kahn and Jan Hoffmann. 2020.  Exponential Automatic Amortized Resource Analysis. In _Foundations of Software Science and Computation Structures_ , Jean Goubault-Larrecq and Barbara König (Eds.). Springer International Publishing, Cham, 359–380.  https://doi.org/10.1007/978-3-030-45231-5_19
  * Kavvos (2017a) G. A. Kavvos. 2017a.  Dual-Context Calculi for Modal Logic. In _Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)_.  arXiv:1602.04860 http://arxiv.org/abs/1602.04860
  * Kavvos (2017b) G. A. Kavvos. 2017b.  _On the Semantics of Intensionality and Intensional Recursion_.  Ph.D. Dissertation.  arXiv:1712.09302
  * Kavvos et al. (2019) G. A. Kavvos, Edward Morehouse, Daniel R. Licata, and Norman Danner. 2019.  Recurrence Extraction for Functional Programs through Call-by-Push-Value.  _Proceedings of the ACM on Programming Languages_ 4, POPL (Dec. 2019).  https://doi.org/10.1145/3371083
  * Krishnaswami et al. (2015) Neelakantan R. Krishnaswami, Pierre Pradic, and Nick Benton. 2015\.  Integrating Linear and Dependent Types. In _POPL ’15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_. Association for Computing Machinery, Mumbai, India, 17–30.
  * Lawvere (1963) F. William Lawvere. 1963\.  _Functorial Semantics of Algebraic Theories_.  Ph.D. Dissertation. Columbia University.
  * Lee et al. (2007) Daniel K. Lee, Karl Crary, and Robert Harper. 2007\.  Towards a Mechanized Metatheory of Standard ML. In _Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_. Association for Computing Machinery, Nice, France, 173–184.  https://doi.org/10.1145/1190216.1190245
  * Levy (2004) Paul Blain Levy. 2004\.  _Call-By-Push-Value: A Functional/Imperative Synthesis (Semantics Structures in Computation, V. 2)_.  Kluwer Academic Publishers, Norwell, MA, USA.
  * Levy (2006) Paul Blain Levy. 2006\.  Call-by-push-value: Decomposing call-by-value and call-by-name.  _Higher-Order and Symbolic Computation_ 19 (2006), 377–414.  https://doi.org/10.1007/s10990-006-0480-6
  * Licata et al. (2017) Daniel R. Licata, Michael Shulman, and Mitchell Riley. 2017\.  A Fibrational Framework for Substructural and Modal Logics. In _2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 84)_ , Dale Miller (Ed.). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 25:1–25:22.  https://doi.org/10.4230/LIPIcs.FSCD.2017.25
  * Mével et al. (2019) Glen Mével, Jacques-Henri Jourdan, and François Pottier. 2019.  Time Credits and Time Receipts in Iris. In _Programming Languages and Systems_ , Luís Caires (Ed.). Springer International Publishing, Cham, 3–29.
  * Nipkow et al. (2021) Tobias Nipkow, Jasmin Blanchette, Manuel Eberl, Alejandro Gómez Londoño, Peter Lammich, Christian Sternagel, Simon Wimmer, and Bohua Zhan. 2021.  _Functional Algorithms, Verified!_ https://functional-algorithms-verified.org
  * Niu and Harper (2020) Yue Niu and Robert Harper. 2020.  Cost-Aware Type Theory. (2020).  arXiv:2011.03660 [cs.PL]
  * Norell (2009) Ulf Norell. 2009\.  Dependently Typed Programming in Agda. In _Proceedings of the 4th International Workshop on Types in Language Design and Implementation_ _(TLDI ’09)_. Association for Computing Machinery, Savannah, GA, USA, 1–2.
  * Okasaki (1998) Chris Okasaki. 1998\.  _Purely Functional Data Structures_.  Cambridge University Press, USA.
  * Pédrot and Tabareau (2019) Pierre-Marie Pédrot and Nicolas Tabareau. 2019.  The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects.  _Proceedings of the ACM on Programming Languages_ 4, POPL (Dec. 2019).  https://doi.org/10.1145/3371126
  * Pfenning (2001) Frank Pfenning. 2001\.  Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. In _Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science_. IEEE Computer Society, Washington, DC, USA, 221–.  http://dl.acm.org/citation.cfm?id=871816.871845
  * Rajani et al. (2021) Vineet Rajani, Marco Gaboardi, Deepak Garg, and Jan Hoffmann. 2021.  A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis.  _Proceedings of the ACM on Programming Languages_ 5, POPL (Jan. 2021).  https://doi.org/10.1145/3434308
  * Rijke et al. (2020) Egbert Rijke, Michael Shulman, and Bas Spitters. 2020\.  Modalities in homotopy type theory.  _Logical Methods in Computer Science_ Volume 16, Issue 1 (Jan. 2020).  https://doi.org/10.23638/LMCS-16(1:2)2020 arXiv:1706.07526 [math.CT]
  * Schultz and Spivak (2019) Patrick Schultz and David I. Spivak. 2019.  _Temporal Type Theory_. Progress in Computer Science and Applied Logic, Vol. 29.  Birkhäuser Basel.  https://doi.org/10.1007/978-3-030-00704-1 arXiv:1710.10258 [math.CT]
  * Spoonhower et al. (2008) Daniel Spoonhower, Guy E. Blelloch, Robert Harper, and Phillip B. Gibbons. 2008.  Space Profiling for Parallel Functional Programs. In _Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming_. Association for Computing Machinery, Victoria, BC, Canada, 253–264.  https://doi.org/10.1145/1411204.1411240
  * Sterling and Angiuli (2021) Jonathan Sterling and Carlo Angiuli. 2021.  Normalization for Cubical Type Theory. In _Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science_. Association for Computing Machinery, New York, NY, USA.  arXiv:2101.11479 [cs.LO]  To appear.
  * Sterling and Harper (2021) Jonathan Sterling and Robert Harper. 2021.  Logical Relations As Types: Proof-Relevant Parametricity for Program Modules.  _J. ACM_ (2021).  arXiv:2010.08599 [cs.PL]  To appear.
  * Stump (2016) Aaron Stump. 2016\.  _Verified Functional Programming in Agda_.  Association for Computing Machinery and Morgan & Claypool.
  * Tarjan (1985) R. Tarjan. 1985\.  Amortized Computational Complexity.  _Siam Journal on Algebraic and Discrete Methods_ 6 (1985), 306–318.
  * Uemura (2019) Taichi Uemura. 2019\.  A General Framework for the Semantics of Type Theory. (2019).  arXiv:1904.04097 [math.CT]
  * Ullrich (2016) Sebastian Andreas Ullrich. 2016\.  _Simple Verification of Rust Programs via Functional Purification_.  Master’s thesis. IPD Snelting.
  * Wang et al. (2017) Peng Wang, Di Wang, and Adam Chlipala. 2017.  TiML: A Functional Language for Practical Complexity Analysis with Invariants.  _Proceedings of the ACM on Programming Languages_ 1, OOPSLA (Oct. 2017).  https://doi.org/10.1145/3133903

##  Appendix A Implementation in Agda

We give a brief overview of the Agda implementation of calf; the codebase and
installation instructions are accessible through the supplementary materials.
We define calf in Agda by postulating the constants in the signature
$\Sigma_{\textbf{calf}{}}$ (see Fig. 3) and animating the associated equations
with the newly added rewriting facilities (Cockx et al., 2021). For instance,
the basic judgmental structure of calf may be specified by the following Agda
postulates and definitions:

[sections/code.tex]lang-g1

[sections/code.tex]lang-g2

[sections/code.tex]lang-g3

[sections/code.tex]lang-g4

An example showcasing the rewriting feature is the inversion principle for
$\mathsf{bind}$:

[sections/code.tex]lang-g5

Observe that the Agda implementation of calf constitutes an algebra (see
Definition 5.1) $\mathcal{A}_{\text{Agda}}$ in which Set plays the role of the
universe of judgments $\bf{Jdg}$.

##### Importing Agda data types

To maximize reuse of the Agda mathematical library, we axiomatize a new
connective to import Agda data types into calf: 888Note that we do not need to
internalize the entire universe Set: in actuality we only use meta to import
types pertaining directly to our case studies, a situation that may be more
objectively described by defining meta on a collection of relevant _type
codes_ that _decode_ into types in Set. For the sake of simplicity, we elide
this distinction in the implementation.

[sections/code.tex]lang-meta

For example, the type of calf natural numbers maybe defined as nat = U (meta
$\mathbb{N}$). Note that we define meta as a connective that internalizes Adga
data types as _computation_ types, a design decision motivated by the fact
that the connective is mostly used in positions where a computation is
expected, _e.g_. when defining a function of the form
$\mathsf{tm}^{+}(A)\to\mathsf{tm}^{\ominus}(\textsf{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}meta}}(\mathbb{N}))$.
Observe that meta generalizes the constants $\widehat{\mathbb{C}}$ and
$\widehat{\leq}$ defined in Fig. 10.

##### Uniform _vs._ nonuniform cost models

In calf, cost analysis with respect to an _algorithm-specific_ cost model may
directly take advantage of the importing mechanism because it is trivial to
instrument the relevant operations with the desired cost _after_ they are
defined in a cost-free manner in Agda. For instance, in the analysis of
Euclid’s algorithm (see Section 4.1) we may directly import the Agda type of
natural numbers $\mathbb{N}$ and the associated modulus function, which we
instrument in calf as $\textit{mod}_{\mathsf{inst}}$. In contrast, a _uniform_
cost model such as the one required in the amortized analysis of batched
queues (see Section 4.2) precludes one from importing the required data type.
In the case of batched queues, it is not possible to define an Agda inductive
type that charges $\mathsf{step}$’s for list iteration, so we must axiomatize
such a cost-aware list type in calf (see Fig. 13).

##  Appendix B Complete definition of calf

$\displaystyle\mathsf{tp}^{+}$ $\displaystyle:\bf{Jdg}$
$\displaystyle\mathsf{tm}^{+}$ $\displaystyle:\mathsf{tp}^{+}\to\bf{Jdg}$
$\displaystyle\mathsf{U}$
$\displaystyle:\mathsf{tp}^{\ominus}\to\mathsf{tp}^{+}$
$\displaystyle\mathsf{F}$
$\displaystyle:\mathsf{tp}^{+}\to\mathsf{tp}^{\ominus}$
$\displaystyle\mathsf{tm}^{\ominus}(X)$
$\displaystyle\coloneqq\mathsf{tm}^{+}(\mathsf{U}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
X$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
X$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
X$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
X$}\mathclose{}{)}})$ $\displaystyle\mathsf{ret}$
$\displaystyle:(A:\mathsf{tp}^{+},a:\mathsf{tm}^{+}(A))\to\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}})$ $\displaystyle\mathsf{bind}$
$\displaystyle:\,\mathrel{\\{A:\mathsf{tp}^{+},X:\mathsf{tp}^{\ominus}\\}}\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}})\to(\mathsf{tm}^{+}(A)\to\mathsf{tm}^{\ominus}(X))\to\mathsf{tm}^{\ominus}(X)$
$\displaystyle\mathsf{tbind}$
$\displaystyle:\,\mathrel{\\{A:\mathsf{tp}^{+}\\}}\to\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}})(\mathsf{tm}^{+}(A)\to\mathsf{tp}^{\ominus})\to\mathsf{tp}^{\ominus}$
$\displaystyle\mathsf{dbind}$
$\displaystyle:\,\mathrel{\\{A:\mathsf{tp}^{+},X:\mathsf{tm}^{+}(A)\mathsf{tp}^{\ominus}\\}}(e:\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}}))\to((a:\mathsf{tm}^{+}(A))\to\mathsf{tm}^{\ominus}(X(a)))\to\mathsf{tm}^{\ominus}(\mathsf{tbind}(e;X))$
Figure 8. Core $\partial\textbf{cbpv}$ calculus.
$\displaystyle\mathsf{bind}/\mathsf{ret}$
$\displaystyle:\,\mathrel{\\{A,X\\}}(a:\mathsf{tm}^{+}(A))\to(f:\mathsf{tm}^{+}(A)\to\mathsf{tm}^{\ominus}(X))\to\mathsf{bind}(\mathsf{ret}(a);f)=f(a)$
$\displaystyle\mathsf{tbind}/\mathsf{ret}$
$\displaystyle:\,\mathrel{\\{A\\}}(a:\mathsf{tm}^{+}(A))\to(f:\mathsf{tm}^{+}(A)\to\mathsf{tp}^{\ominus})\to\mathsf{tbind}(\mathsf{ret}(a);f)=f(a)$
$\displaystyle\mathsf{dbind}/\mathsf{ret}$
$\displaystyle:\,\mathrel{\\{A,X\\}}(a:\mathsf{tm}^{+}(A))\to(f:a:\mathsf{tm}^{+}(A)\to\mathsf{tm}^{\ominus}(X(a)))\to\mathsf{dbind}(\mathsf{ret}(a);f)=f(a)$
$\displaystyle\mathsf{bind}/\mathsf{assoc}$
$\displaystyle:\,\mathrel{\\{A,B,X\\}}(e:\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}}))\to$
$\displaystyle(f:\mathsf{tm}^{+}(A)\to\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
B$}\mathclose{}{)}}))\to(g:\mathsf{tm}^{+}(B)\to\mathsf{tm}^{\ominus}(C))\to$
$\displaystyle\mathsf{bind}(\mathsf{bind}(e;f);g)=\mathsf{bind}(e;\lambda
a.\,\mathsf{bind}(f(a);g))$ $\displaystyle\mathsf{tbind}/\mathsf{assoc}$
$\displaystyle:\,\mathrel{\\{A,B,X\\}}(e:\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}}))\to(f:\mathsf{tm}^{+}(A)\to\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
B$}\mathclose{}{)}}))\to$
$\displaystyle\mathsf{tbind}(\mathsf{bind}(e;f);X)=\mathsf{tbind}(e;\lambda
a.\,\mathsf{tbind}(f(a);X))$ Figure 9. Computation and associativity laws for
sequencing. $\displaystyle\begin{aligned} \mathbb{C}&:\bf{Jdg}\\\
0&:\mathbb{C}\\\ +&:\mathbb{C}\to\mathbb{C}\to\mathbb{C}\\\
\leq&:\mathbb{C}\to\mathbb{C}\to\bf{Jdg}{}\\\
\mathsf{costMon}&:\mathsf{isCostMonoid}(\mathbb{C},0,+,\leq)\end{aligned}\qquad\begin{aligned}
\widehat{\mathbb{C}}&:\mathsf{tp}^{\ominus}\\\
(\mathsf{out}_{\mathbb{C}},\mathsf{in}_{\mathbb{C}})&:\mathsf{tm}^{\ominus}(\widehat{\mathbb{C}})\cong\mathbb{C}\\\
\widehat{\leq}&:\widehat{\mathbb{C}}\to\widehat{\mathbb{C}}\to\mathsf{tp}^{\ominus}\\\
(\mathsf{out}_{\leq},\mathsf{in}_{\leq})&:\,\mathrel{\\{c,c^{\prime}\\}}\mathsf{tm}^{\ominus}(c\mathrel{\widehat{\leq}}c^{\prime})\cong(\mathsf{out}_{\mathbb{C}}(c)\leq\mathsf{out}_{\mathbb{C}}(c^{\prime}))\end{aligned}$
$\displaystyle\begin{aligned}
\mathsf{step}&:\,\mathrel{\\{X:\mathsf{tp}^{\ominus}\\}}\mathbb{C}\to\mathsf{tm}^{\ominus}(X)\to\mathsf{tm}^{\ominus}(X)\\\
\mathsf{step}_{0}&:\,\mathrel{\\{X,e\\}}\mathsf{step}^{0}(e)=e\\\
\mathsf{step}_{+}&:\,\mathrel{\\{X,e,c_{1},c_{2}\\}}\mathsf{step}^{c_{1}}(\mathsf{step}^{c_{2}}(e))=\mathsf{step}^{c_{1}+c_{2}}(e)\end{aligned}$
$\displaystyle\begin{aligned}
\mathsf{bind}_{\mathsf{step}}&:\,\mathrel{\\{A,X,e,f,c\\}}\mathsf{bind}(\mathsf{step}^{c}(e);f)=\mathsf{step}^{c}(\mathsf{bind}(e;f))\\\
\mathsf{tbind}_{\mathsf{step}}&:\,\mathrel{\\{A,X,e,f,c\\}}\mathsf{tbind}(\mathsf{step}^{c}(e);f)=\mathsf{tbind}(e;f)\\\
\mathsf{dbind}_{\mathsf{step}}&:\,\mathrel{\\{A,X,e,f,c\\}}\mathsf{dbind}(\mathsf{step}^{c}(e);f)=\mathsf{step}^{c}(\mathsf{dbind}(e;f))\\\
\end{aligned}$ Figure 10. Cost structure and cost effect.
$\displaystyle\P_{\mathsf{E}}$ $\displaystyle:\bf{Jdg}$
$\displaystyle\P_{\mathsf{E}}/{\mathsf{uni}}$
$\displaystyle:\,\mathrel{\\{u,v:\P_{\mathsf{E}}\\}}u=v$
$\displaystyle\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}}$ $\displaystyle\coloneqq\P_{\mathsf{E}}\to A$
$\displaystyle\mathsf{step}/{\P_{\mathsf{E}}}$
$\displaystyle:\,\mathrel{\\{X,e,c\\}}\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathsf{step}^{c}(e)=e$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathsf{step}^{c}(e)=e$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathsf{step}^{c}(e)=e$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathsf{step}^{c}(e)=e$}\mathclose{}{)}}$
$\displaystyle\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}^{+}$
$\displaystyle:\mathsf{tp}^{+}\to\mathsf{tp}^{+}$ $\displaystyle\\_$
$\displaystyle:\,\mathrel{\\{A\\}}\mathsf{tm}^{+}(\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}^{+}{A})\cong\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}(\mathsf{tm}^{+}(A))$
🌑 $\displaystyle:\mathsf{tp}^{+}\to\mathsf{tp}^{+}$
$\displaystyle\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}$
$\displaystyle:\mathsf{tm}^{+}(A)\to\mathsf{tm}^{+}(\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}{A})$
$\displaystyle\ast$
$\displaystyle:\P_{\mathsf{E}}\to\mathsf{tm}^{+}(\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}{A})$
$\displaystyle\\_$ $\displaystyle:\Pi a:\mathsf{tm}^{+}(A).\,\Pi
u:\P_{\mathsf{E}}.\,\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}(a)=\ast(u)$
$\displaystyle\mathsf{ind}_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}$
$\displaystyle:\,\mathrel{\\{A\\}}(a:\mathsf{tm}^{+}(\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}{A}))\to(X:\mathsf{tm}^{+}(\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}{A})\to\mathsf{tp}^{\ominus})\to$
$\displaystyle(x_{0}:(a:\mathsf{tm}^{+}(A))\to\mathsf{tm}^{\ominus}(X(\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}(a))))\to$
$\displaystyle(x_{1}:(u:\P_{\mathsf{E}})\to\mathsf{tm}^{\ominus}(X(\ast(u))))\to$
$\displaystyle((a:\mathsf{tm}^{+}(A))\to(u:\P_{\mathsf{E}})\to
x_{0}(a)=x_{1}(u))\to$ $\displaystyle\mathsf{tm}^{\ominus}(X(a))$
$\displaystyle\mathsf{ind}_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}/\eta$
$\displaystyle:\,\mathrel{\\{A\\}}(a:\mathsf{tm}^{+}(A))\to(X:\mathsf{tm}^{+}(\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}{A})\to\mathsf{tp}^{\ominus})\to$
$\displaystyle(x_{0}:(a:\mathsf{tm}^{+}(A))\to\mathsf{tm}^{\ominus}(X(\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}(a))))\to$
$\displaystyle(x_{1}:(u:\P_{\mathsf{E}})\to\mathsf{tm}^{\ominus}(X(\ast(u))))\to$
$\displaystyle(h:(a:\mathsf{tm}^{+}(A))\to(u:\P_{\mathsf{E}})\to
x_{0}(a)=x_{1}(u))\to$
$\displaystyle\mathsf{ind}_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}(\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}(a),X,x_{0},x_{1},h)=x_{0}(a)$
$\displaystyle\mathsf{ind}_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}/\ast$
$\displaystyle:\,\mathrel{\\{A\\}}(u:\P_{\mathsf{E}})\to(X:\mathsf{tm}^{+}(\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}{A})\to\mathsf{tp}^{\ominus})\to$
$\displaystyle(x_{0}:(a:\mathsf{tm}^{+}(A))\to\mathsf{tm}^{\ominus}(X(\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}(a))))\to$
$\displaystyle(x_{1}:(u:\P_{\mathsf{E}})\to\mathsf{tm}^{\ominus}(X(\ast(u))))\to$
$\displaystyle(h:(a:\mathsf{tm}^{+}(A))\to(u:\P_{\mathsf{E}})\to
x_{0}(a)=x_{1}(u))\to$
$\displaystyle\mathsf{ind}_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}(\ast(u),X,x_{0},x_{1},h)=x_{1}(u)$
Figure 11. Modal account of the phase distinction. $\displaystyle\Pi$
$\displaystyle:(A:\mathsf{tp}^{+},X:\mathsf{tm}^{+}(A)\to\mathsf{tp}^{\ominus})\to\mathsf{tp}^{\ominus}$
$\displaystyle(\mathsf{ap},\mathsf{lam})$
$\displaystyle:\,\mathrel{\\{A,X\\}}\mathsf{tm}^{\ominus}(\Pi(A;X))\cong(a:\mathsf{tm}^{+}(A))\to\mathsf{tm}^{\ominus}(X(a))$
$\displaystyle\Sigma^{++}$
$\displaystyle:(A:\mathsf{tp}^{+},B:\mathsf{tm}^{+}(A)\to\mathsf{tp}^{+})\to\mathsf{tp}^{+}$
$\displaystyle(\mathsf{unpair}^{++},\mathsf{pair}^{++})$
$\displaystyle:\,\mathrel{\\{A,B\\}}\mathsf{tm}^{+}(\Sigma^{++}(A;B))\cong\Sigma(\mathsf{tm}^{+}(A))(\lambda
a.\,\mathsf{tm}^{+}(B(a)))$ $\displaystyle\Sigma^{+-}$
$\displaystyle:(A:\mathsf{tp}^{+},X:\mathsf{tm}^{+}(A)\to\mathsf{tp}^{\ominus})\to\mathsf{tp}^{\ominus}$
$\displaystyle(\mathsf{unpair}^{+-},\mathsf{pair}^{+-})$
$\displaystyle:\,\mathrel{\\{A,X\\}}\mathsf{tm}^{\ominus}(\Sigma^{+-}(A;X))\cong\Sigma(\mathsf{tm}^{+}(A))(\lambda
a.\,\mathsf{tm}^{\ominus}(X(a)))$ $\displaystyle\mathsf{eq}$
$\displaystyle:(A:\mathsf{tp}^{+})\to\mathsf{tm}^{+}(A)\to\mathsf{tm}^{+}(A)\to\mathsf{tp}^{+}$
$\displaystyle\mathsf{self}$
$\displaystyle:\,\mathrel{\\{A\\}}(a,b:\mathsf{tm}^{+}(A))\to
a=_{\mathsf{tm}^{+}(A)}b\to\mathsf{tm}^{+}(\mathsf{eq}_{A}(a,b))$
$\displaystyle\mathsf{ref}$
$\displaystyle:\,\mathrel{\\{A\\}}(a,b:\mathsf{tm}^{+}(A))\to\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathsf{eq}_{A}(a,b)$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathsf{eq}_{A}(a,b)$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathsf{eq}_{A}(a,b)$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathsf{eq}_{A}(a,b)$}\mathclose{}{)}})\to
a=_{\mathsf{tm}^{+}(A)}b$ $\displaystyle\mathsf{uni}$
$\displaystyle:\,\mathrel{\\{A,a,b\\}}(p,q:\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathsf{eq}_{A}(a,b)$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathsf{eq}_{A}(a,b)$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathsf{eq}_{A}(a,b)$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathsf{eq}_{A}(a,b)$}\mathclose{}{)}}))\to\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}{(p=q)}$
$\displaystyle 1$ $\displaystyle:\mathsf{tp}^{+}$ $\displaystyle\star$
$\displaystyle:\mathsf{tm}^{+}(1)$ $\displaystyle\eta_{1}$
$\displaystyle:\,\mathrel{\\{u,v\\}}u=_{\mathsf{tm}^{+}(1)}v$ $\displaystyle+$
$\displaystyle:\mathsf{tp}^{+}\to\mathsf{tp}^{+}\to\mathsf{tp}^{+}$
$\displaystyle\mathsf{inl}$
$\displaystyle:\,\mathrel{\\{A,B\\}}\mathsf{tm}^{+}(A)\to\mathsf{tm}^{+}(A+B)$
$\displaystyle\mathsf{inr}$
$\displaystyle:\,\mathrel{\\{A,B\\}}\mathsf{tm}^{+}(B)\to\mathsf{tm}^{+}(A+B)$
$\displaystyle\mathsf{case}$
$\displaystyle:\,\mathrel{\\{A,B\\}}(s:\mathsf{tm}^{+}(A+B))\to(\mathsf{tm}^{+}(A+B)\to\mathsf{tp}^{\ominus})\to$
$\displaystyle((a:\mathsf{tm}^{+}(A))\to\mathsf{tm}^{\ominus}(X(\mathsf{inl}(a))))\to$
$\displaystyle((b:\mathsf{tm}^{+}(B))\to\mathsf{tm}^{\ominus}(X(\mathsf{inl}(b))))\to\mathsf{tm}^{\ominus}(X(s))$
$\displaystyle\mathsf{case}_{\mathsf{inl}}$
$\displaystyle:\,\mathrel{\\{A,B,X,e_{0},e_{1}\\}}(a:\mathsf{tm}^{+}(A))\to\mathsf{case}(\mathsf{inl}(a);X;e_{0};e_{1})=e_{0}(a)$
$\displaystyle\mathsf{case}_{\mathsf{inr}}$
$\displaystyle:\,\mathrel{\\{A,B,X,e_{0},e_{1}\\}}(b:\mathsf{tm}^{+}(B))\to\mathsf{case}(\mathsf{inr}(b);X;e_{0};e_{1})=e_{1}(b)$
$\displaystyle\mathsf{nat}$ $\displaystyle:\mathsf{tp}^{+}$
$\displaystyle\mathsf{zero}$ $\displaystyle:\mathsf{tm}^{+}(\mathsf{nat})$
$\displaystyle\mathsf{suc}$
$\displaystyle:\mathsf{tm}^{+}(\mathsf{nat})\to\mathsf{tm}^{+}(\mathsf{nat})$
$\displaystyle\mathsf{rec}$
$\displaystyle:(n:\mathsf{tm}^{+}(\mathsf{nat}))\to(X:\mathsf{tm}^{+}(\mathsf{nat})\to\mathsf{tp}^{\ominus})\to\mathsf{tm}^{\ominus}(X(\mathsf{zero}))\to$
$\displaystyle((n:\mathsf{tm}^{+}(\mathsf{nat}))\to\mathsf{tm}^{\ominus}(X(n))\to\mathsf{tm}^{\ominus}(X(\mathsf{suc}(n))))\to\mathsf{tm}^{\ominus}(X(n))$
$\displaystyle\mathsf{rec}/\mathsf{zero}$
$\displaystyle:\,\mathrel{\\{X,e_{0},e_{1}\\}}\mathsf{rec}(\mathsf{zero};X;e_{0};e_{1})=e_{0}$
$\displaystyle\mathsf{rec}/\mathsf{suc}$
$\displaystyle:\,\mathrel{\\{n,X,e_{0},e_{1}\\}}\mathsf{rec}(\mathsf{suc}(n);X;e_{0};e_{1})=e_{1}(n)(\mathsf{rec}(n;X;e_{0};e_{1}))$
Figure 12. Types $\displaystyle\mathsf{L}$
$\displaystyle:{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}\mathbb{C}}\to\mathsf{tp}^{+}\to\mathsf{tp}^{+}$
$\displaystyle\mathsf{nil}$
$\displaystyle:\,\mathrel{\\{c,A\\}}\mathsf{L}^{c}(A)$
$\displaystyle\mathsf{cons}$
$\displaystyle:\,\mathrel{\\{c,A\\}}\mathsf{tm}^{+}(A)\to\mathsf{tm}^{+}(\mathsf{L}^{c}(A))\to\mathsf{tm}^{+}(\mathsf{L}^{c}(A))$
$\displaystyle\mathsf{rec}$
$\displaystyle:\,\mathrel{\\{c,A\\}}(l:\mathsf{tm}^{+}(\mathsf{L}^{c}(A)))\to(X:\mathsf{tm}^{+}(\mathsf{L}^{c}(A))\to\mathsf{tp}^{\ominus})\to$
$\displaystyle(\mathsf{tm}^{\ominus}(X(\mathsf{nil})))\to$
$\displaystyle((a:\mathsf{tm}^{+}(A))\to(l:\mathsf{tm}^{+}(\mathsf{L}^{c}(A)))\to\mathsf{tm}^{\ominus}(X(l))\to\mathsf{tm}^{\ominus}(X(\mathsf{cons}(a;l))))\to$
$\displaystyle\mathsf{tm}^{\ominus}(X(l))$
$\displaystyle\mathsf{rec}/\mathsf{nil}$
$\displaystyle:\,\mathrel{\\{c,A,X,e_{0},e_{1}\\}}\mathsf{rec}_{\mathsf{L}}(\mathsf{nil};X;e_{0};e_{1})=e_{0}$
$\displaystyle\mathsf{rec}/\mathsf{cons}$
$\displaystyle:\,\mathrel{\\{c,A,a,X,e_{0},e_{1}\\}}(l:\mathsf{tm}^{+}(\mathsf{L}^{c}(A)))\to$
$\displaystyle\mathsf{rec}_{\mathsf{L}}(\mathsf{cons}(a;l);X;e_{0};e_{1})={\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}\mathsf{step}^{c}}(e_{1}(a)(l)(\mathsf{rec}_{\mathsf{L}}(l;X;e_{0};e_{1})))$
Figure 13. Types, continued $\displaystyle\mathsf{lam}_{\mathsf{step}}$
$\displaystyle:\,\mathrel{\\{A,X,c\\}}(f:(a:\mathsf{tm}^{+}(A))\to\mathsf{tm}^{\ominus}(X(a)))\to\mathsf{step}^{c}(\mathsf{lam}(f))=\mathsf{lam}(\mathsf{step}^{c}(f))$
$\displaystyle\mathsf{pair}^{+-}_{\mathsf{step}}$
$\displaystyle:\,\mathrel{\\{A,X,c\\}}(e:\Sigma(\mathsf{tm}^{+}(A))(\lambda
a.\,\mathsf{tm}^{\ominus}(X(a))))\to\mathsf{step}^{c}(e)=(e\cdot
1,\mathsf{step}^{c}(e\cdot 2))$ $\displaystyle\mathsf{case}_{\mathsf{step}}$
$\displaystyle:\,\mathrel{\\{A,B,X,e_{0},e_{1},c\\}}(s:\mathsf{tm}^{+}(A+B))\to$
$\displaystyle\mathsf{step}^{c}(\mathsf{case}(s;X;e_{0};e_{1}))=\mathsf{case}(s;X;\lambda
a.\,\mathsf{step}^{c}(e_{0}(a));\lambda b.\,\mathsf{step}^{c}(e_{1}(b)))$
Figure 14. Interaction of $\mathsf{step}$ with type structure.
$\displaystyle\&$
$\displaystyle:\,\mathrel{\\{A,B:\mathsf{tp}^{+}\\}}\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}})\to\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
B$}\mathclose{}{)}})\to\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A\times B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle A\times
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle A\times
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle A\times
B$}\mathclose{}{)}})$ $\displaystyle\&_{\mathsf{join}}$
$\displaystyle:\,\mathrel{\\{A,B,c_{1},c_{2},a,b\\}}\left(\mathsf{step}^{c_{1}}(\mathsf{ret}(a))\right)\mathrel{\&}\left(\mathsf{step}^{c_{2}}(\mathsf{ret}(b))\right)=\mathsf{step}^{c_{1}\otimes
c_{2}}(\mathsf{ret}((a,b)))$ Figure 15. Parallelism.