Martin-Löf Clashes With Griffin, Operationally (2009)
Abstract. The computational reading of proofs in intutionistic predicate logic (IPL) as λ-terms can be extended in two well-known ways. On the one hand, Martin-Löf showed how the Axiom of Choice...
Abstract. We make an argument that, for any study involving computational effects such as divergence or continuations, the traditional syntax of simply typed lambda-calculus cannot be regarded as...
Call-By-Push-Value: Decomposing Call-By-Value And Call-By-Name (2008)
We present the call-by-push-value (CBPV) calculus, which decomposes the typed call-by-value (CBV) and typed call-by-name (CBN) paradigms into fine-grain primitives. On the operational side, we give...
Jumping Semantics For Call-By-Push-Value (2008)
Abstract. We give a jumping machine for a higher-order language, embodying the intuition that calling a procedure is a jump, and returning from a procedure is also a jump. The machine makes it very...
Infinitary Howe's Matrix (2008)
Howe’s method is a well-known technique for proving that various kinds of applicative bisimilarity (or similarity) on a functional language are congruences (or precongruences). It proceeds by...
Abstract Infinite Trace Equivalence (2008)
We solve a longstanding problem by providing a denotational model for nondeterministic programs that identifies two programs iff they have the same range of possible behaviours. We discuss the...
Abstract. We make an argument that, for any study involving computational effects such as divergence or continuations, the traditional syntax of simply typed lambda-calculus cannot be regarded as...
Monads and Adjunctions for Global Exceptions Abstract (2008)
In this paper, we look at two categorical accounts of computational effects (strong monad as a model of the monadic metalanguage, adjunction as a model of call-bypush-value with stacks), and we adapt...
Abstract MFPS XX1 Preliminary Version Infinite Trace Equivalence (2008)
We solve a longstanding problem by providing a denotational model for nondeterministic programs that identifies two programs iff they have the same range of possible behaviours. We discuss the...
Paul Blain Levy, Paul Blain Levy
Call-by-push-value (CBPV) is a new programming language paradigm, based on the slogan “a value is, a computation does”. We claim that CBPV provides the semantic primitives from which the...
Combining algebraic effects with continuations (2008)
Martin Hyl, Paul Blain Levy, Gordon Plotkin, John Power
Abstract. We consider the natural combinations of algebraic computational effects such as side-effects, exceptions, interactive input/output, and nondeterminism with continuations. Continuations are...
Soren Lassen, Paul Blain Levy, Parametricity Isomorphisms, B Fa
In µX.A and νX.A we require A to be covariant in X.
Combining Continuations with Other Effects (2007)
Martin Hyland, Paul Blain Levy, Gordon Plotkin, John Power
A fundamental question, in modelling computational effects, is how to give a unified semantic account of modularity, i.e., a mathematical theory that supports the various combinations one naturally...
• SOREN: NEED TO CHANGE FUNCTION APPLI- CATION SYNTAX TO OPERAND-FIRST EVERY- WHERE (2007)
Soren B. Lassen, Google Inc, A Def, B Def, Paul Blain Levy
This note uses the normal form bisimulation theory for recursively typed call-by-push-value (CBPV) [1] to prove a “syntactic minimal invariance ” result.
Combining algebraic effects with continuations (2007)
Hyland, Martin, Levy, Paul Blain, Plotkin, Gordon, Power, Anthony
Adjunction models for call-by-push-value with stacks (2005)
Call-by-push-value is a ”semantic machine code”, providing a set of simple primitives from which both the call-by-value and call-by-name paradigms are built. We present its operational semantics...
Eager normal form bisimulation (2005)
Soren 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...
Abstract. Call-by-push-value is a ”semantic machine code”, providing a set of simple primitives from which both the call-by-value and call-by-name paradigms are built. We present its operational...
Abstract. Call-by-push-value is a ”semantic machine code”, providing a set of simple primitives from which both the call-by-value and call-by-name paradigms are built. We present its operational...
Divergenceleast semantics of amb is Hoare (2005)
Soren B. Lassen, Paul Blain Levy, Prakash Panangaden
Abstract This note strengthens the hoary observation that McCarthy’s amb is not monotone with respect to the Smyth and Plotkin powerdomains. It shows that there is no least fixpoint semantics for...
Combining Continuations with Other Effects (2004)
Martin Hyl, Paul Blain Levy, Gordon Plotkin, John Power
A fundamental question, in modelling computational effects, is how to give a unified semantic account of modularity, i.e., a mathematical theory that supports the various combinations one naturally...
Modelling Environments in Call-By-Value Programming Languages (2002)
Paul Blain Levy, John Power, Hayo Thielecke
this paper, we investigate environments in call-by-value languages by analysing a fine-grain variant of Moggi's computational #- calculus, giving two equivalent sound and complete classes of...
Paul Blain Levy, Paul Blain Levy, Paul Blain Levy
Call-by-push-value (CBPV) is a new programming language paradigm, based on the slogan “a value is, a computation does”. We claim that CBPV provides the semantic primitives from which the...
Call-by-Push-Value: A Subsuming Paradigm (1999)
Abstract. Call-by-push-value is a new paradigm that subsumes the call-by-name and call-by-value paradigms, in the following sense: both operational and denotational semantics for those paradigms can...
Call-By-Push-Value: A Subsuming Paradigm (1999)
Call-by-push-value is a new paradigm that subsumes the call-by-name and call-by-value paradigms, in the following sense: both operational and denotational semantics for those paradigms can be seen as...