constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
internalization and categorical algebra
algebra object (associative, Lie, …)
internal category ($\to$ more)
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In a category with internal homs $[-,-]$, given an object $S$, the continuation monad is the endofunctor $X \mapsto [[X, S], S]$.
In computer science this monad (in computer science) is used to model continuation-passing style of programming, and therefore this is called the continuation monad. The idea here is that a morphism $f \colon X \to Y$ in the Kleisli category of the continuation monad, hence a morphism in the original category of the form $X\longrightarrow [[Y,S],S]$ is much like a map from $X$ to $Y$ only that instead of “returning” its output directly it instead feeds it into a given function $Y \to S$ which hence continues the computation.
As a monad in computer science:
The continuation monad is discussed in the generality of linear type theory as the linear double negation monad in
Paul-André Melliès, Nicolas Tabareau, Linear continuation and duality, 2008 (pdf)
Paul-André Melliès, The parametric continuation monad, Mathematical Structures in Computer Science, Festschrift in honor of Corrado Böhm for his 90th birthday (2013). (pdf)
Last revised on November 6, 2022 at 09:57:38. See the history of this page for a list of all contributions to it.