https://bentnib.org/paramnotions-jfp.pdf

Moggi’s Computational Monads and Power et al ’s equivalent notion of Freyd category have captured a large range of computational effects present in programming languages. Examples include non-termination, non-determinism, exceptions, continuations, side-effects and input/output. We present generalisations of both computational monads and Freyd categories, which we call parameterised monads and parameterised Freyd categories, that also capture computational effects with parameters. Examples of such are composable continuations, side-effects where the type of the state varies and input/output where the range of inputs and outputs varies. By also considering structured parameterisation, we extend the range of effects to cover separated side-effects and multiple independent streams of I/O. We also present two typed λ-calculi that soundly and completely model our categorical definitions — with and without symmetric monoidal parameterisation — and act as prototypical languages with parameterised effects.

http://www-verimag.imag.fr/~riegl/thesis/thesis-print.pdf

A major breakthrough came with Timothy Griffin in 1990 [Gri90] who removed this restriction and extended the correspondence to classical logic through the callcc control operator [SS75] which captures the state of the environment. Intuitively, callcc allows us to go back in time to a previous point in the program and to make a different choice, i.e. take a different execution path. Although Peter Landin earlier introduced a control operator J [Lan65a, Lan65b] to explain the behavior of the goto instruction of Algol60 [BBG+60], Timothy Griffin was the first to type a control operator. This discovery is specially remarkable because it connects callcc and Peirce’s law which were both known for a long time, respectively thirty years and over a century, and that such a deep connection was never noticed before. Following this result, various techniques have been used to encompass classical logic into computation: classical λ-calculi like Michel Parigot’s λμ-calculus [Par92], Stefano Berardi’s interactive realizability [AB10] and Jean-Louis Krivine’s classical realizability [Kri09] to name a few. This document will focus on the last one.

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.51.8448&rep=rep1&type=pdf

This paper addresses the problem of extending the formulae-as-types principle to classical logic. More precisely, we introduce a typed lambda-calculus (λ-LK→) whose inhabited types are exactly the implicative tautologies of classical logic and whose type assignment system is a classical sequent calculus. Intuitively, the terms of λ-LK→ correspond to constructs that are highly non-deterministic. This intuition is made much more precise by providing a simple model where the terms of λ-LK→ are interpreted as non-empty sets of (interpretations of) untyped lambda-terms. We also consider the system (λ-LK→ + cut) and investigate the relation existing between cut elimination and reduction. Finally, we show how to extend our system in order to take conjunction, disjunction and negation into account.

http://sro.sussex.ac.uk/id/eprint/1439/1/streicherreus1998.pdf

One of the goals of this paper is to demonstrate that denotational semantics is useful for operational issues like implementation of functional languages by abstract machines. This is exemplified in a tutorial way by studying the case of extensional untyped call-by- name λ-calculus with Felleisen’s control operator C. We derive the transition rules for an abstract machine from a continuation semantics which appears as a generalization of the ¬¬-translation known from logic. The resulting abstract machine appears as an extension of Krivine’s machine implementing head reduction. Though the result, namely Krivine’s machine, is well known our method of deriving it from continuation semantics is new and applicable to other languages (as e.g. call-by-value variants). Further new results are that Scott’s D∞-models are all instances of continuation models. Moreover, we extend our continuation semantics to Parigot’s λμ-calculus from which we derive an extension of Krivine’s machine for λμ-calculus. The relation between continuation semantics and the abstract machines is made precise by proving computational adequacy results employing an elegant method introduced by Pitts.

http://www.nuprl.org/documents/Murthy/EvaluationSemantics.pdf

https://ieeexplore.ieee.org/document/151634

It is shown how to interpret classical proofs as programs in a way that agrees with the well-known treatment of constructive proofs as programs and moreover extends it to give a computational meaning to proofs claiming the existence of a value satisfying a recursive predicate. The method turns out to be equivalent to H. Friedman's (Lecture Notes in Mathematics, vol.699, p.21-28, 1978) proof by A-transition of the conservative extension of classical cover constructive arithmetic for II/sub 2//sup 0/ sentences. It is shown that Friedman's result is a proof-theoretic version of a semantics-preserving CPS-translation from a nonfunctional programming language back to a functional programming language. A sound evaluation semantics for proofs in classical number theory (PA) of such sentences is presented as a modification of the standard semantics for proofs in constructive number theory (HA). The results soundly extend the proofs-as-programs paradigm to classical logics and to programs with the control operator, C

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.84.1959&rep=rep1&type=pdf

Haskell Is Not Not ML

Ben Rudiak-Gould, Alan Mycroft1, and Simon Peyton Jones

Abstract.

We present a typed calculus IL (“intermediate language”) which supports the embedding of ML-like (strict, eager) and Haskell-like (non-strict, lazy) languages, without favoring either. IL’s type system includes negation (continuations), but not implication (function arrow). Within IL we find that lifted sums and products can be represented as the double negation of their unlifted counterparts. We exhibit a compilation function from IL to AM—an abstract von Neumann machine—which maps values of ordinary and doubly negated types to heap structures resembling those found in practical implementations of languages in the ML and Haskell families. Finally, we show that a small variation in the design of AM allows us to treat any ML value as a Haskell value at runtime without cost, and project a Haskell value onto an ML type with only the cost of a Haskell deepSeq. This suggests that IL and AM may be useful as a compilation and execution model for a new language which combines the best features of strict and non-strict functional programming.

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 ).