Categorical proof theory of classical propositional calculus (2008)
Gianluigi Bellin, Martin Hyland, Edmund Robinson, Christian Urban C
We investigate semantics for classical proof based on the sequent calculus. We show that the propositional connectives are not quite well-behaved from a traditional categorical perspective, and give...
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...
Categorical Combinatorics for Innocent Strategies (2007)
Harmer, Russ, Hyland, Martin, Melliès, Paul-André
We show how to construct the category of games and innocent strategies from a more primitive category of games. On that category we define a comonad and monad with the former distributing over the...
Categorical Combinatorics for Innocent Strategies (2007)
Harmer, Russ, Hyland, Martin, Melliès, Paul-André
We show how to construct the category of games and innocent strategies from a more primitive category of games. On that category we define a comonad and monad with the former distributing over the...
Combining algebraic effects with continuations (2007)
Hyland, Martin, Levy, Paul Blain, Plotkin, Gordon, Power, Anthony
Categorical Proof Theory of Classical Propositional Calculus (2005)
Gianluigi Bellin, Martin Hyland, Edmund Robinson, Christian Urban C
We investigate semantics for classical proof based on the sequent calculus. We show that the propositional connectives are not quite well-behaved from a traditional categorical perspective, and give...
Combining computational effects: commutativity and sum (2003)
Hyland, Martin, Plotkin, Gordon, Power, John
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...
Combining computational effects: commutativity and sum (2003)
Hyland, Martin, Plotkin, Gordon, Power, John
We begin to develop a unified account of modularity for com- putational eects. We use the notion of enriched Lawvere theory, to- gether with its relationship with strong monads, to reformulate...
Glueing and orthogonality for models of linear logic (2003)
We present the general theory of the method of glueing and associated technique of orthogonality for constructing categorical models of all the structure of linear logic: in particular we treat the...
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...
Designs, Disputes and Strategies (2002)
Claudia Faggian, Martin Hyland
Ludics has been proposed by Girard as an abstract general approach to proof theory. We explain how its basic notions correspond to those of the \innocent strategy" appraoch to Games Semantics,...
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...
Games on graphs and sequentially realizable functionals (2002)
We present a new category of games on graphs and derive from it a model for Intuitionistic Linear Logic. Our category has the computational flavour of concrete data structures but embeds fully and...
Games on Graphs and Sequentially Realizable Functionals (2002)
Exte Nd Ed, Martin Hyland, Andrea Schalk
Martin Hyland DPMMS Centre for Mathematical Sciences Wilberforce Road, Cambridge, CB3 0WB, UK M.Hyland@dpmms.cam.ac.uk Andrea Schalk Department of Computer Science University of Manchester Oxford...
Traced Premonoidal Categories (1999)
Motivated by some examples from functional programming, we propose a generalization of the notion of trace to symmetric premonoidal categories and of Conway operators to Freyd categories. We show...
A Term Calculus for Intuitionistic Linear Logic (1993)
Nick Benton, Gavin Bierman, Valeria De Paiva, Martin Hyland
. 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. Our...
Dialogue Games and Innocent Strategies: An Approach to (Intensional) Full Abstraction for PCF (1993)
ion for PCF Preliminary Announcement Martin Hyland and Luke Ong 26th July 1993 This note is (intended to be) released in conjunction with a preliminary announcement of Abramsky, Jagadeesan and...
Linear lambda-Calculus and Categorical Models Revisited (1992)
Nick Benton, Gavin Bierman, Valeria De Paiva, Martin Hyland
this paper we shall consider multiplicative exponential linear logic (MELL), i.e. the fragment which has multiplicative conjunction or tensor,\Omega , linear implication, \Gammaffi, and the logical...
Term assignment for intuitionistic linear logic (1992)
Nick Benton, Gavin Bierman, Valeria Paiva, Martin Hyland
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. Our system...
Term Assignment for Intuitionistic Linear Logic (Preliminary Report) (1992)
Nick Benton, Gavin Bierman, Valeria De Paiva, Martin Hyland
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. Our system...
A Syntactic Characterization of the Equality in some Models for the Lambda Calculus (1976)
An equality relation on the terms of the A-calculus is an equivalence relation closed under the (syntactical) operations of application and A-abstraction. We may distinguish between syntactic and...