Continuation models are universal for λμ-calculus

https://www.researchgate.net/publication/3707355_Continuation_models_are_universal_for_lm-calculus

We show that a certain simple call-by-name continuation semantics of Parigot's λ_μ-calculus (1992) is complete. More precisely, for every λμ-theory we construct a cartesian closed category such that the ensuing continuation-style interpretation of λ_μ, which maps terms to functions sending abstract continuations to responses, is full and faithful. Thus, any λ_μ-category in the sense of is isomorphic to a continuation model derived from a cartesian-closed category of continuations

A Formulae-as-Types Interpretation of Subtractive Logic

https://www.semanticscholar.org/paper/A-Formulae-as-Types-Interpretation-of-Subtractive-Crolard/5c4363af97178d0ed468b6dc83b377a4f874fde6

https://pdfs.semanticscholar.org/5c43/63af97178d0ed468b6dc83b377a4f874fde6.pdf

A Formulae-as-Types Interpretation of Subtractive Logic

The computational interpretation of classical logic is usually given by a λ-calculus extended with some form of control (such as the famous call/cc of Scheme or the catch/throw mechanism of Lisp) or similar formulations of first-class continuation constructs. Continuations are used in denotational semantics to describe control commands such as jumps. They can also be used as a programming technique to simulate backtracking and coroutines. For instance, first-class continuations have been successfully used to implement Simula-like cooperative coroutines in Scheme [53, 18, 19]. This approach has been extended in the Standard ML of New Jersey (with the typed counterpart of Scheme’s call/cc [15]) to provide simple and elegant implementations of light-weight processes (or threads), where concurrency is obtained by having individual threads voluntarily suspend themselves [48, 42] (providing time-sliced processes using pre-emptive scheduling requires additional run-time system support [5, 47]). The key point in these implementations is that control operators make it possible to switch between coroutine contexts, where the context of a coroutine is encoded as its continuation.

The definition of a catch/throw mechanism is straightforward in the λμ-calculus: just
set catch α t ≡ μα[α]t and throw α t ≡ μδ[α]t where δ is a name which does not occur in t (see [7] for a study of the sublanguage obtained when we restrict the λμ-terms to these
operators). Then a name α may be reified as the first-class continuation λx.throw α x.
However, the type of such a λμ-term is the excluded-middle ⊢ Aα; ¬A. Thus, a continuation cannot be a first-class citizen in a constructive logic. To figure out what kind of second-order logic, in which ∨ , ∧ , ∃, ∃ are definable from → , ∀, ∀ . Since we are also interested in the subformula property, we shall restrict ourselves to the propositional framework where any connective is taken as primitive and where the proof normalization process includes permutative conversions [12]. Such an extension of CND with primitive conjunction and disjunction has already been investigated by Pym, Ritter and Wallen [40, 41, 39] and de Groote [12].
restricted use of continuations is allowed in SND→∨∧, we observe that in the restricted →+×λμ -calculus, even if continuations are no longer first-class objects, the ability of context-switching remains (in fact, this observation is easier to make in the framework of abstract state machines). However, a context is now a pair ⟨environment, continuation⟩.
Note that such a pair is exactly what we expect as the context of a coroutine, since a
coroutine should not access the local environment (the part of the environment which is
→+× not shared) of another coroutine. Consequently, we say that a λμ -term t is safe with
respect to coroutine contexts (or just safe for short) if no coroutines of t access the local environment of another coroutine.
The extension of this interpretation to SND→∨∧− is now straightforward. We already
know (from its definition in classical logic) that subtraction is a good candidate to type a
pair ⟨environment, continuation⟩. SND→∨∧− is thus interpreted as a type system for →+×−
first-class coroutines. The dual restriction from the safe λμ -calculus just ensures that one cannot obtain full-fledged first-class continuations back from first-class coroutines.

If we forget about linearity (which has of course many consequences on the resulting system), the main advantages of our approach are the following ones:
• We propose a computational interpretation of our restriction (as coroutines which do not access the local environment on another coroutine ).
• Our restriction is symmetrical and thus easily extends to duality. This allows us to propose a computational interpretation of subtraction (as a type constructor for first-class coroutines ).