Pseudo-distributive laws (2008)
Eugenia Cheng A, Martin Hyl, John Power B
We address the question of how elegantly to combine a number of different structures, such as finite product structure, monoidal structure, and colimiting structure, on a category. Extending work of...
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...
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...
Technical Report Number 535 Designs, disputes and strategies (2007)
Claudia Faggian, C Claudia Faggian, Martin Hyl, Martin Hyl
Important progresses in logic are leading to interactive and dynamical models. Geometry of Interaction and Games Semantics are two major examples. Ludics, initiated by Girard, is a further step in...
hour talks, two invited short courses and forty-eight contributed papers. There were also (2007)
Richard Bornat, The Dov Gabbay, Wilfrid Hodges, Martin Hyl, Thomas Jech, David Makinson, ...
demonstrations of computerized logic teaching software, by Stephen Read, Steve Reeves
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...
Wellfounded Trees and Dependent Polynomial Functors (2004)
Abstract. We set out to study the consequences of the assumption of types of wellfounded trees in dependent type theories. We do so by investigating the categorical notion of wellfounded tree...
A term calculus for intuitionistic linear logic (1993)
Nick Benton, Gavin Bierman, Valeria De Paiva, Martin Hyl
Abstract. In this paper we consider the problem of deriving a term assignment system for Girard's Intuitionistic Linear Logic for both the sequent calculus and natural deduction proof systems....
Linear -calculus and categorical models revisited (1992)
Nick Benton, Gavin Bierman, Valeria De Paiva, Martin Hyl
In this paper we shall consider multiplicative exponential linear logic (MELL), i.e. the fragment which has multiplicative conjunction or tensor, \Omega, linear implication, \Gamma ffi, and the...