Tensors of Comodels and Models for Operational Semantics (2009)
In seeking a unified study of computational effects, in particular in order to give a general operational semantics agreeing with the standard one for state, one must take account of the coalgebraic...
Generic Models for Computational Effects (2009)
A Freyd-category is a subtle generalisation of the notion of a category with finite products. It is suitable for modelling environments in call-by-value programming languages, such as the...
We outline a possible logic that will allow us to give a unified approach to reasoning about computational effects. The logic is given by extending Moggi’s computational λ-calculus by basic types...
Abstract A Coalgebraic Foundation for Linear Time Semantics (2008)
We present a coalgebraic approach to trace equivalence semantics based on lifting behaviour endofunctors for deterministic action to Kleisli categories of monads for non-deterministic choice. In Set,...
Combining computational effects: commutativity and sum (2008)
Martin Hyl, Gordon Plotkin, John Power
Abstract. We begin to develop a unified account of modularity for computational effects. We use the notion of enriched Lawvere theory, together with its relationship with strong monads, to...
Combining effects: sum and tensor (2008)
Martin Hyl, Gordon Plotkin, John Power
Abstract. We seek a unified account of modularity for computational effects. We begin by reformulating Moggi’s monadic paradigm for modelling computational effects using the notion of enriched...
Edinburgh EH9 3JZ Scotland (2008)
We outline a possible logic that will allow us to give a unified approach to reasoning about computational effects. The logic is given by extending Moggi’s computational λ-calculus by basic types...
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...
MFPS 17 Preliminary Version Semantics for algebraic operations (2008)
Abstract Given a category C with finite products and a strong monad T on C, we investigate axioms under which an ObC-indexed family of operations of the form ffx: (T x)n-! T x provides a definitive...
Abstract MFPS 17 Preliminary Version Semantics for algebraic operations (2008)
Given a category C with finite products and a strong monad T on C, we investigate axioms under which an ObC-indexed family of operations of the form αx: (T x) n − → T x provides a definitive...
Fibrational semantics for many-valued logic programs: grounds for non-groundness. (2008)
Komendantskaya, Ekaterina, Power, John
We introduce a fibrational semantics for many-valued logic programming, use it to define an SLD-resolution for annotation-free many valued logic programs as defined by Fitting, and...
Fibrational semantics for many-valued logic programs: grounds for non-groundness. (2008)
Komendantskaya, Ekaterina, Power, John
We introduce a fibrational semantics for many-valued logic programming, use it to define an SLD-resolution for annotation-free many valued logic programs as defined by Fitting, and...
Combining a Monad and a Comonad (2007)
We give a systematic treatment of distributivity for a monad and a comonad as arises in giving category theoretic accounts of operational and denotational semantics, and in giving an intensional...
John Power Edinburgh, January 1995 (2007)
January Comments Are, John Power
control structures do not have an explicit set of names, and they fit more naturally into the usual use of category theory in computer science, particularly in denotational semantics. Here, we go one...
A Representation Result for Free (2007)
Free Cocompletions, Gian Luca Cattani, Glynn Winskel, John Power, John Power
et al.: A
Whilst the relationship between initial algebras and monads is well-understood, the relationship between nal coalgebras and comonads is less well explored. This paper shows that the problem is more...
Combining computational e#ects: commutativity and sum Martin Hyland, (2007)
Abstract. We begin to develop a unified account of modularity for computational e#ects. We use the notion of enriched Lawvere theory, together with its relationship with strong monads, to reformulate...
King's Buildings, Edinburgh EH9 3JZ Scotland (2007)
We develop a notion of equivalence between interpretations of the simply typed -calculus together with an equationally de ned abstract data-type, and we show that two interpretations are equivalent...
MFPS 17 Preliminary Version An Algebraic Foundation for Graph-based Diagrams in Computing (2007)
We develop an algebraic foundation for some of the graph-based structures underlying a variety of popular diagrammatic notations for the specication, modelling and programming of computing systems....
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...
Edinburgh EH9 3JZ Scotland (2007)
We outline a possible logic that will allow us to give a unied approach to reasoning about computational eects. The logic is given by extending Moggi's computational -calculus by basic types and...
Abstracts for Presentations Edited by (2007)
Magne Haveraaen, John Power, Monika Seisenberger, John Power, Monika Seisenberger
CALCO brings together researchers and practitioners to exchange new results related to foundational aspects and both traditional and emerging uses of algebras and coalgebras in computer science. The...
Magne Haveraaen, John Power, Magne Haveraaen, John Power, Monika Seisenberger
The CALCO Young Researchers Workshop, CALCO-jnr, was a satellite event for 2nd Conference on Algebra and Coalgebra in Computer Science, August 20-24, 2007, Bergen, Norway (CALCO’07). CALCO-jnr was...
Coalgebraic semantics for timed processes (2006)
Marco Kick, John Power, Alex Simpson
We give a coalgebraic formulation of timed processes and their operational semantics. We model time by a monoid called a “time domain”, and we model processes by “timed transition systems”,...
A Unified Category-theoretic Semantics for Binding Signatures in Substructural Logics (2006)
Generalizing Fiore et al.'s use of the category 𝔽 of finite sets to model untyped Cartesian contexts and Tanaka's use of the category ℙ of permutations to model untyped linear contexts, we...
Thesis (MSc--Geology)--University of Auckland, 2005.
Peter Mosses, John Power, Monika Seisenberger, John Power, Monika Seisenberger
and WADT – the Workshop on Algebraic Development Techniques, have joined their forces and reputations into a new high-level bi-annual conference. Starting in 2005, CALCO brings together researchers...
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...
Algebraic Operations and Generic Effects (2003)
Given a complete and cocomplete symmetric monoidal closed category V and a symmetric monoidal V-category C with cotensors and a strong V-monad T on C, we investigate axioms under which an ObC-indexed...
Algebraic Operations and Generic Effects (2003)
Abstract. Given a complete and cocomplete symmetric monoidal closed category V and a symmetric monoidal V-category C with cotensors and a strong V-monad T on C, we investigate axioms under which an...
Combining effects: Sum and tensor (2003)
Martin Hyland, Gordon Plotkin, John Power
Abstract. We seek a unified account of modularity for computational effects. We begin by reformulating Moggi's monadic paradigm for modelling computational effects using the notion of enriched...
Dualising initial algebras. Coalgebraic methods in computer science (Genova, 2001) (2003)
Ghani, Neil, Lüth, Christoph, De Marchi, Federico, Power, John
Notions of computation determine monads (2002)
Abstract. We give semantics for notions of computation, also called computational e#ects, by means of operations and equations. We show that these generate several of the monads of primary interest...
Combining Computational Effects: Commutativity and Sum (2002)
Martin Hyland, Gordon Plotkin, John Power
We begin to develop a unified account of modularity for computational effects. We use the notion of enriched Lawvere theory, together with its relationship with strong monads, to reformulate...
Notions of Computation Determine Monads (2002)
We model notions of computation using algebraic operations and equations. We show that these generate several of the monads of primary interest that have been used to model computational e#ects, with...
Computational Effects and Operations: An Overview (2002)
We overview a programme to provide a unified semantics for computational effects based upon the notion of a countable enriched Lawvere theory. We define the notion of countable enriched Lawvere...
Notions of computation determine monads (2002)
Abstract. We model notions of computation using algebraic operations and equations. We show that these generate several of the monads of primary interest that have been used to model computational...
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...
Semantics for algebraic operations (2001)
Abstract. Given a complete and cocomplete symmetric monoidal closed category V and a symmetric monoidal V-category C with cotensors and a strong V-monad T on C, we investigate axioms under which an...
Adequacy for Algebraic Effects (2001)
Abstract. Moggi proposed a monadic account of computational effects. He also presented the computational λ-calculus, λc, a core call-by-value functional programming language for effects; the...
Semantics for Algebraic Operations (2001)
Given a category C with finite products and a strong monad T on C, we investigate axioms under which an ObC-indexed family of operations of the form Tx provides a definitive semantics for algebraic...
Adequacy for Algebraic Effects (2001)
Moggi proposed a monadic account of computational effects. He also presented the computational λ-calculus...
On the structure of categories of coalgebras (2001)
Johnstone, Peter, Power, John, Tsujishita, Toru, Watanabe, Hiroshi, Worrell, James
Distributivity for Endofunctors, Pointed and Co-Pointed Endofunctors, Monads and Comonads (2000)
Marina Lenisa, John Power, Hiroshi Watanabe
We generalise the notion of a distributive law between a monad and a comonad to consider weakened structures such as pointed or co-pointed endofunctors, or endofunctors. We investigate...
Distributivity for Endofunctors, Pointed and Co-Pointed Endofunctors, Monads and Comonads (2000)
Marina Lenisa, John Power, Hiroshi Watanabe
We generalise the notion of a distributive law between a monad and a comonad to consider weakened structures such as pointed or co-pointed endofunctors, or endofunctors. We investigate...
Gordon Plotkin, John Power, Donald Sannella, Robert Tennent
Lax logical relations are a categorical generalisation of logical relations; though they preserve product types, they need not preserve exponential types. But, like logical relations, they are...
Data Refinement and Algebraic Structure (2000)
We recall Hoare's formulation of data refinement in terms of upward, downward and total simulations between locally ordered functors from the structured locally ordered category generated by a...
Gordon Plotkin, John Power, Donald Sannella, Robert Tennent
Lax logical relations are a categorical generalisation of logical relations; though they preserve product types, they need not preserve exponential types. But, like logical relations, they are...
Gordon Plotkin, John Power, Donald Sannella, Robert Tennent
Abstract. Lax logical relations are a categorical generalisation of logical relations; though they preserve product types, they need not preserve exponential types. But, like logical relations, they...
Enriched Lawvere Theories (1999)
. We define the notion of enriched Lawvere theory, for enrichment over a monoidal biclosed category V that is locally finitely presentable as a closed category. We prove that the category of enriched...
Closed Freyd- and k-Categories (1999)
. We give two classes of sound and complete models for the computational -calculus, or c-calculus. For the first, we generalise the notion of cartesian closed category to that of closed...
A Coalgebraic Foundation for Linear Time Semantics (1999)
We present a coalgebraic approach to trace equivalence semantics based on lifting behaviour endofunctors for deterministic action to Kleisli categories of monads for non-deterministic choice. In Set...
Closed Freyd- and k-Categories (1999)
. We give two classes of sound and complete models for the computational -calculus, or c-calculus. For the first, we generalise the notion of cartesian closed category to that of closed...
A categorical axiomatics for bisimulation (1998)
John Power, Glynn Winskel, Gian Luca Cattani, Gian Luca Cattani
et al.: A
A Categorical Axiomatics for Bisimulation (1998)
Gian Luca Cattani, John Power, Glynn Winskel
. We give an axiomatic category theoretic account of bisimulation in process algebras based on the idea of functional bisimulations as open maps. We work with 2-monads, T , on Cat. Operations on...
An Axiomatics for Categories of Transition Systems as Coalgebras (1998)
Peter Johnstone, John Power, Toru Tsujishita, James Worrell
We consider a finitely branching transition system as a coalgebra for an endofunctor on the category Set of small sets. A map in that category is a functional bisimulation. So, we study the structure...
An Axiomatics for Categories of Coalgebras (1998)
We give an axiomatic account of what structure on a category C and an endofunctor H on C yield similar structure on the category H0Coalg of H-coalgebras. We give conditions under which completeness,...
A Compositional Generalisation of Logical Relations (1998)
Gordon Plotkin John, John Power, Don Sannella
Binary logical relations do not compose. So we generalise the notion of logical relation to one of lax logical relation, so that binary lax logical relations do compose. We give both a direct...
A Compositional Generalisation of Logical Relations (1998)
Gordon Plotkin, John Power, Don Sannella
Binary logical relations do not compose. So we generalise the notion of logical relation to one of lax logical relation, so that binary lax logical relations do compose. We give both a direct...
This document in subdirectoryRS/98/22/ A Categorical Axiomatics for Bisimulation (1998)
Gian Luca Cattani, John Power, Glynn Winskel, Gian Luca Cattani, John Power, Glynn Winskel
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent BRICS...
This document in subdirectoryRS/98/21/ A Representation Result for Free (1998)
Free Cocompletions, John Power, Gian Luca Cattani, Glynn Winskel, John Power, Gian Luca Cattani, ...
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent BRICS...
Complete Cuboidal Sets in Axiomatic Domain Theory (Extended Abstract) (1997)
Marcelo Fiore, Gordon Plotkin, John Power
) Marcelo Fiore !mf@dcs.ed.ac.uk? Gordon Plotkin y !gdp@dcs.ed.ac.uk? John Power !ajp@dcs.ed.ac.uk? Department of Computer Science Laboratory for Foundations of Computer Science University of...
Environments, Continuation Semantics and Indexed Categories (1997)
. There have traditionally been two approaches to modelling environments, one by use of ønite products in Cartesian closed categories, the other by use of the base categories of indexed categories...
Logical relations and data abstraction (1996)
Abstract. We prove, in the context of simple type theory, that logical relations are sound and complete for data abstraction as given by equational speci cations. Specically, we show that two...
Data Refinement and Algebraic Structure (1996)
We recall Hoare's formulation of data refinement in terms of upward, downward and total simulations between locally ordered functors from the structured locally ordered category generated by a...
Lax Naturality Through Enrichment (1995)
We develop the relationship between algebraic structure and monads enriched over the monoidal biclosed category LocOrd l of small locally ordered categories, with closed structure given by Lax(A; B)....
Alex Mifsud Robin, Robin Milner, John Power
Action calculi have been defined as a broad class of action structures with added structure; they are syntactic in nature. Each action calculus AC(K) is determined essentially by a set K of controls....
We define the notion of enriched Lawvere theory, for enrichment over a monoidal biclosed category V that is locally finitely presentable as a closed category. We prove that the category of enriched...
Distributivity for a Monad and a Comonad
We give a systematic treatment of distributivity for a monad and a comonad as arises in incorporating category theoretic accounts of operational and denotational semantics, and in giving an...
This document in subdirectoryNS/98/7/ Contents 2-Categories
See back inner page for a list of recent BRICS Notes Series publications. Copies may be obtained by contacting: BRICS