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 , the continuation monad is the endofunctor .
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 in the Kleisli category of the continuation monad, hence a morphism in the original category of the form is much like a map from to only that instead of “returning” its output directly it instead feeds it into a given function which hence continues the computation.
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 December 30, 2020 at 05:27:19. See the history of this page for a list of all contributions to it.