\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{call-by-push-value}

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{syntax}{Syntax}\dotfill \pageref*{syntax} \linebreak
\noindent\hyperlink{judgmental_structure}{Judgmental Structure}\dotfill \pageref*{judgmental_structure} \linebreak
\noindent\hyperlink{type_structure}{Type Structure}\dotfill \pageref*{type_structure} \linebreak
\noindent\hyperlink{shifts}{Shifts}\dotfill \pageref*{shifts} \linebreak
\noindent\hyperlink{as_an_adjoint_logic}{As an Adjoint Logic}\dotfill \pageref*{as_an_adjoint_logic} \linebreak
\noindent\hyperlink{related}{Related}\dotfill \pageref*{related} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

Call-by-push-value is a type theory and programming language which contains full embeddings of [[call-by-value]] and [[call-by-name]], including their operational semantics and equational theories.

Its semantics decomposes the semantics of effectful languages using a [[strong monad]] into a [[strong adjunction]]. Then the embeddings of call-by-value and call-by-name correspond to the construction of [[Kleisli category|Kleisli and co-Kleisli categories]] from an adjunction.

\hypertarget{syntax}{}\subsection*{{Syntax}}\label{syntax}

\hypertarget{judgmental_structure}{}\subsubsection*{{Judgmental Structure}}\label{judgmental_structure}

CBPV has two ``kinds'' of types: value types, written $A,A',A_i$ and computation types written $B,B',B_i$. As originally presented there are 3 term judgments of CBPV: Values, Terms, and Stacks.

The value judgment is an ordinary simple type theory. A context $\Gamma$ is a sequence of value typed variables $x_1:A_1,\ldots$ and the judgment $\Gamma \vdash V : A$ admits symmetry, contraction, weakening and the corresponding substitution principle: if for every $x_i:A_i$ in $\Gamma$, $\Gamma' \vdash \gamma(x_i) : A_i$, then there is a value $\Gamma' \vdash V[\gamma] : A$.

The term judgment has again a value typed context $\Gamma$, but the output type is a computation type $\Gamma \vdash M : B$. Again it admits symmetry, contraction and weakening, and admits a substitution principle on its inputs, if we have a $\gamma$ as above, then there is a term $\Gamma' \vdash M[\gamma] : B$.

Finally the stack judgment has a value context $\Gamma$ as input, but also a computation type as input and output: $\Gamma | B \vdash S : B'$. Stacks have an admissible substitution operation $S[\gamma]$ as above. Stacks also have a composition operation: if $\Gamma | B \vdash S : B'$ and $\Gamma | B' \vdash S' : B''$ then $\Gamma | B \vdash S'[S] : B''$, which is associative and has a unit: the empty stack $\Gamma | B \vdash \bullet : B$. Finally, stacks have an action on terms: if $\Gamma \vdash M : B$ and $\Gamma | B \vdash S : B'$ then $\Gamma \vdash S[M] : B'$, which is associative with $\bullet$ as identity.

We can get a slightly simpler presentation by combining the stack and term judgments into a single term judgment with a [[stoup]]: a context that is either a single type $B$ or empty. Then a term as before is a term typed with the empty stoup and a stack is a term typed with a full stoup. This has the benefit of combining the action of stacks on terms and the composition of stacks as one operation. Below we write a stoup as $\Delta$, and if it is empty we don't write it at all.

\hypertarget{type_structure}{}\subsubsection*{{Type Structure}}\label{type_structure}

Call-by-push-value is characterized not just by its judgmental structure, but by a specific \emph{choice} of which connectives to use. Except for the shifts $F,U$, all value type connectives are left adjoints, and all computation type connectives are right adjoints.

For this reason, some connectives are definable from the judgments but excluded because they violate this discipline. These are a tensor product $A \otimes B$ which is a computation type, a unit $I$ computation type, and a linear function space $B \multimap B'$ which is a computation type. When these are added, the system is called the \hyperlink{EEC}{Enriched Effect Calculus} (modulo some superficial syntactic differences).

\hypertarget{shifts}{}\paragraph*{{Shifts}}\label{shifts}

The shift types express the adjunction between values and stacks. The type $UB$ is a value type that is pronounced as ``thunk of $B$'', and can be thought of as the type of [[closures]] that when called behave as $B$. It is a value type, but a right adjoint, with invertible introduction rule

\begin{displaymath}
\frac { \Gamma \vdash M : B }
         { \Gamma \vdash thunk M : UB }
\end{displaymath}
and elimination rule:

\begin{displaymath}
\frac { \Gamma \vdash V : UB }
         { \Gamma \vdash force V : B }
\end{displaymath}
With $\beta$ rule $force thunk M = M$ and $\eta$ rule $V = thunk force V$.

The type $FA$ is a computation type that is the type of ``returners of $A$s''. It is a computation type, but a left adjoint, with invertible elimination rule that enables the sequencing of effects:

\begin{displaymath}
\frac { \Gamma | \Delta \vdash M : F A \qquad \Gamma, x : A \vdash N : B}
         { \Gamma | \Delta \vdash M to x. N : B }
\end{displaymath}
with introduction rule:

\begin{displaymath}
\frac {\Gamma \vdash V : A } { \Gamma \vdash return V : F A }
\end{displaymath}
with $\beta$ rule $(return V) to x. N = N[V/x]$ and $\eta$ rule that for any stack $\Gamma | F A \vdash S : B$, we have $S = \bullet to x. S[return x]$.

\hypertarget{as_an_adjoint_logic}{}\subsection*{{As an Adjoint Logic}}\label{as_an_adjoint_logic}

The semantics of Call-by-push-value was originally presented using fibred categories, but we can get a presentation of its semantics in a more multi-categorical flavor by expressing it as an [[adjoint logic]] from a specific mode theory in the sense of \hyperlink{LSR}{LSR}.

As a summary, the mode theory of CBPV is the theory of a cartesian monoid acting on a pointed object. In more detail, we have two modes: $v$ for values and $c$ for computations. Then the $v$ mode is axiomatized as a cartesian monoid $(v,\times,1)$, which gives the value judgment. To axiomatize the term and stack judgments, we add an asymmetric tensor product

\begin{displaymath}
a:v,b:c \vdash a\otimes b : c
\end{displaymath}
to represent the combined context $\Gamma \pipe B$ and also a ``point'' for the computation types:

\begin{displaymath}
\vdash i : c
\end{displaymath}
which represents the empty stoup.

To correctly model the substitution structure, we add equations that say that the tensor product constitutes an action of the monoid, i.e., associativity and unitality:

\begin{displaymath}
(a \times a') \otimes b = a \otimes (a' \otimes b) \qquad 1 \otimes b = b
\end{displaymath}
Then for example, the $F$ type above is $F_{x \otimes i}$ and the $U$ type is $U_{x. x \otimes i}$.

Furthermore, the mode theory also gives the ``missing'' types of the Enriched Effect Calculus. The tensor product is $F_{x \otimes y}$, the unit is $F_{i}$ and the linear function space is $U_{x. x\otimes y}$.

Note that this mode theory is equivalent to the one given for a strong monad in \hyperlink{LSR}{LSR}, which instead of the point $i$ adds a morphism $a : v \vdash g(a) : c$, and requires this be a homomorphism of $v$-actions in that

\begin{displaymath}
g(a \times b) = a \otimes g(b)
\end{displaymath}
However, this is equivalent to our above presentation because for any $a:v$, we have $a = a \times 1$, so $g(a) = g(a \times 1) = a\otimes g(1)$, so $g$ is completely determined by where it takes $1$, so we can axiomatize that directly as the point $i$.

\hypertarget{related}{}\subsection*{{Related}}\label{related}

\begin{itemize}%
\item The linear term judgment in [[linear-non-linear logic]] can be seen as extending the call-by-push-value stack judgment to allow for ``multi-hole'' stacks.

\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

\begin{itemize}%
\item [[Paul-Blain Levy]], \href{https://link.springer.com/chapter/10.1007/3-540-48959-2_17}{\emph{Call-by-Push-Value: A Subsuming Paradigm}, TLCA 1999}


\item [[Paul-Blain Levy]], \href{https://www.cs.bham.ac.uk/~pbl/papers/ctcs02journal.pdf}{Adjunction Models for Call-by-push-value with Stacks\_, CTCS 2003}


\item Jeff Egger, Rasmus Ejlers Møgelberg and Alex Simpson, \href{http://homepages.inf.ed.ac.uk/als/Research/Sources/eec.pdf}{The Enriched Effect Calculus: Syntax and Semantics} Journal of Logic and Computation, Volume 24.


\item [[Daniel Licata]], [[Mike Shulman]], and [[Mitchell Riley]], \emph{A Fibrational Framework for Substructural and Modal Logics (extended version)}, in Proceedings of 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) (\href{http://drops.dagstuhl.de/opus/volltexte/2017/7740/}{doi: 10.4230/LIPIcs.FSCD.2017.25}, \href{http://dlicata.web.wesleyan.edu/pubs/lsr17multi/lsr17multi-ex.pdf}{pdf})



\end{itemize}


\end{document}