Author name cluster

Paul Blain Levy

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

2 author rows

TCS Journal 2007 Journal Article

Combining algebraic effects with continuations

Martin Hyland
Paul Blain Levy
Gordon Plotkin
John Power

We consider the natural combinations of algebraic computational effects such as side-effects, exceptions, interactive input/output, and nondeterminism with continuations. Continuations are not an algebraic effect, but previously developed combinations of algebraic effects given by sum and tensor extend, with effort, to include commonly used combinations of the various algebraic effects with continuations. Continuations also give rise to a third sort of combination, that given by applying the continuations monad transformer to an algebraic effect. We investigate the extent to which sum and tensor extend from algebraic effects to arbitrary monads, and the extent to which Felleisen et al. ’s C operator extends from continuations to its combination with algebraic effects. To do all this, we use Dubuc’s characterisation of strong monads in terms of enriched large Lawvere theories.

Details DOI

CSL Conference 2007 Conference Paper

Typed Normal Form Bisimulation

Søren B. Lassen
Paul Blain Levy

Abstract Normal form bisimulation is a powerful theory of program equivalence, originally developed to characterize Lévy-Longo tree equivalence and Boehm tree equivalence. It has been adapted to a range of untyped, higher-order calculi, but types have presented a difficulty. In this paper, we present an account of normal form bisimulation for types, including recursive types. We develop our theory for a continuation-passing style calculus, Jump-With-Argument (JWA), where normal form bisimilarity takes a very simple form. We give a novel congruence proof, based on insights from game semantics. A notable feature is the seamless treatment of eta-expansion. We demonstrate the normal form bisimulation proof principle by using it to establish a syntactic minimal invariance result and the uniqueness of the fixed point operator at each type.

Details

CSL Conference 2002 Conference Paper

Possible World Semantics for General Storage in Call-By-Value

Paul Blain Levy

Abstract We describe a simple denotational semantics, using possible worlds, for a call-by-value language with ML-like storage facilities, allowing the storage of values of any type, and the generation of new storage cells. We first present a criticism of traditional Strachey semantics for such a language: that it requires us to specify what happens when we read non-existent cells. We then obtain our model by modifying the Strachey semantics to avoid this problem. We describe our model in 3 stages: first no storage of functions or recursion (but allowing storage of cells), then we add recursion, and finally we allow storage of functions. We discuss similarities and differences between our model and Moggi’s model of ground store. A significant difference is that our model does not use monadic decomposition of the function type.

Details