\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*{continuation-passing style}

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

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{continuation_semantics}{Continuation semantics}\dotfill \pageref*{continuation_semantics} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


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

In the theory of [[programming languages]], the idea that procedures may be modelled as mathematical [[functions]] is useful for compositional reasoning, but at first seems to rule out programming with more sophisticated control structures which can actually be very useful in practice. For example, we might want to write an integer division routine which raises an exception on division-by-zero, or a procedure that lazily computes the first satisfying assignment to a boolean formula while giving the user the ability to query to obtain additional ones.

Now, an ``impure'' functional language such as OCaml lets us do some of this directly. For example, we can write the following code for integer division:

\begin{verbatim}let divide : int -> int -> int =
  fun x y -> if y == 0 then raise Division_by_zero else x / y\end{verbatim}
However, it should be said that the type ascription ``'' is a bit misleading here (or at least open to misinterpretation), since  cannot actually be modelled as a set-theoretic function of type $\mathbb{Z} \to \mathbb{Z} \to \mathbb{Z}$.

\emph{Continuation-passing style} (or CPS) is a very general technique that allows one to express many different seemingly ``non-functional'' patterns of control flow within the confines of pure functional programming. The basic idea is that a procedure in CPS takes an additional argument (often named ``$k$'') representing the \emph{continuation}, a functional abstraction of the context in which the procedure is used (or ``the rest of the computation''). Whenever a procedure in ``direct style'' would return a value ($v$), the corresponding procedure in CPS instead invokes the continuation with that value ($k(v)$). However, it is the fact that the procedure has explicit access to the continuation which also allows for the possibility of exceptional behaviors, typically by throwing away the continuation or by invoking it more than once.

To transform the example above into continuation-passing style, first we must fix an ``answer type'', that is, the return type of the continuation. In this case, to allow for the possibility of raising a division-by-zero error, the answer type should be a [[pointed type]]. For example, we could take

\begin{verbatim}type ans = int option\end{verbatim}
Now, our division routine can be written as follows in CPS:

\begin{verbatim}let divide_cps : int -> int -> (int -> ans) -> ans =
  fun x y k -> if y == 0 then None else k (x / y)\end{verbatim}
Observe that we have replaced the (somewhat misleading) original type

\begin{verbatim}divide : int -> int -> int\end{verbatim}
by the more complicated type

\begin{verbatim}divide_cps : int -> int -> (int -> ans) -> ans\end{verbatim}
This may be recognized as a form of [[double negation translation]], and indeed under [[propositions as types]], the classical negative translations correspond to different forms of continuation-passing style transformations. Under this correspondence, the ``answer type'' corresponds to the type of [[false|absurdity]] $\bot$, but as the above example shows, we almost never want the answer type to be [[empty type|empty]]. As such, CPS translation is best understood in terms of the negative translations from [[classical logic]] into [[minimal logic]], where the type of falsehood $\bot$ behaves like a fixed atomic proposition.

\hypertarget{continuation_semantics}{}\subsection*{{Continuation semantics}}\label{continuation_semantics}

Whereas ``continuation-passing style'' refers to a programming technique, the term ``continuation semantics'' refers to a certain way of assigning [[denotational semantics]] to programs, originally in the context of [[domain theory]] \hyperlink{StracheyWadsworth74}{(Strachey \& Wadsworth 1974)}. The two are very closely related, though, especially if one views the meaning function - in a denotational semantics as a ``definitional interpreter'' in the sense of \hyperlink{Reynolds72}{(Reynolds 1972)}. In that case, giving a continuation semantics for a language corresponds to writing the definitional interpreter in continuation-passing style.

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[continuation monad]]


\item [[programming language]]


\item [[functional programming]]


\item [[Yoneda lemma]]


\item [[negative translation]]


\item \href{excluded+middle#DoubleNegatedPEM}{double-negated principle of excluded middle}


\item [[monad (in computer science)]]


\item [[defunctionalization]], often used in conjunction with continuation-passing style



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

Some early and historical references for continuations and continuation-passing style include:

\begin{itemize}%
\item [[John C. Reynolds]]. Definitional interpreters for higher-order programming languages. In \emph{Proceedings of the ACM National Conference}, 1972. (\href{http://surface.syr.edu/cgi/viewcontent.cgi?article=1012&context=lcsmith_other}{pdf})


\item Christopher Strachey and C. P. Wadsworth. Continuations: A Mathematical Semantics for Handling Full Jumps, Technical Monograph PRG-11, Oxford, 1974. (\href{http://repository.readscheme.org/ftp/papers/plsemantics/oxford/strachey-continuations.PDF}{pdf})


\item [[John C. Reynolds]]. On the Relation Between Direct and Continuation Semantics. Second Colloquium on Automata, Languages, and Programming, Saarbrucken, July 29 - August 2, 1974. (\href{http://repository.cmu.edu/cgi/viewcontent.cgi?article=2287&context=compsci}{pdf})


\item [[Gordon Plotkin]]. Call-by-name, call-by-value, and the lambda-calculus. \emph{Theoretical Computer Science} 1 (1975), 125-159. (\href{http://homepages.inf.ed.ac.uk/gdp/publications/cbn_cbv_lambda.pdf}{pdf})


\item [[John C. Reynolds]]. The Discoveries of Continuations. \emph{LISP and Symbolic Computation} 6 (1993), 233-247. (\href{http://www.math.bas.bg/bantchev/place/iswim/conti-disco.pdf}{pdf})



\end{itemize}
Other references include:

\begin{itemize}%
\item [[Hayo Thielecke]]. \emph{Categorical Structure of Continuation Passing Style}. PhD thesis, University of Edinburgh, 1997. (\href{http://www.lfcs.inf.ed.ac.uk/reports/97/ECS-LFCS-97-376/ECS-LFCS-97-376.pdf}{pdf})


\item [[Josh Berdine]], [[Peter O'Hearn]], [[Uday Reddy]], [[Hayo Thielecke]]. Linear Continuation-Passing. \emph{Higher-Order and Symbolic Computation} 15 (2002), 181-208. (\href{http://research.microsoft.com/pubs/64171/LinCP.pdf}{pdf})


\item [[Ulrich Schöpp]]. On the Relation of Interaction Semantics to Continuations and Defunctionalization. \emph{Logical Methods in Computer Science} Vol.10(4:10)2014, 1-41. (\href{http://arxiv.org/pdf/1410.4980.pdf}{pdf})


\item Wikipedia, \emph{\href{http://en.wikipedia.org/wiki/Continuation-passing_style}{Continuation-passing style}}



\end{itemize}
For the connection between CPS and the [[Yoneda lemma]], see

\begin{itemize}%
\item Ralf Hinze, Daniel W. H. James, \emph{Reason Isomorphically!}, sections 3-4, \href{http://www.cs.ox.ac.uk/ralf.hinze/publications/WGP10.pdf}{pdf}


\item Mike Stay, \emph{The Continuation Passing Transform and the Yoneda Embedding}, \href{https://golem.ph.utexas.edu/category/2008/01/the_continuation_passing_trans.html}{blog post}



\end{itemize}
[[!redirects continuation passing style]]

[[!redirects continuation-passing]] [[!redirects continuation passing]]

[[!redirects continuation semantics]]



\end{document}