Harish Devarajan, Dominic Hughes
We prove full completeness of multiplicative linear logic (MLL) without MIX under the Chu interpretation. In particular we show that the cut-free proofs of MLL theorems are in a natural bijection...
Dominic Hughes, James Warren, Orkut Buyukkokten
We introduce a technique which, given any text input system A and novice user u, will predict the peak expert input speed of u on A, avoiding the costly process of actually training u up to expert...
Hypergames and full completeness for system F (rough draft) (2008)
This paper reviews the fully complete hypergames model of system $F$, presented a decade ago in the author's thesis. Instantiating type variables is modelled by allowing ``games as moves''. The...
Simple multiplicative proof nets with units (2005)
This paper presents a simple notion of proof net for multiplicative linear logic with units. Cut elimination is direct and strongly normalising, in contrast to previous approaches which resorted to...
Simple free star-autonomous categories and full coherence (2005)
This paper gives a simple presentation of the free star-autonomous category over a category, based on Eilenberg-Kelly-MacLane graphs and Trimble rewiring, for full coherence.
A classical sequent calculus free of structural rules (2005)
Gentzen's system LK, classical sequent calculus, has explicit structural rules for contraction and weakening. They can be absorbed (in a right-sided formulation) by replacing the axiom P,not(P) by...
This paper presents an abstract, mathematical formulation of classical propositional logic. It proceeds layer by layer: (1) abstract, syntax-free propositions; (2) abstract, syntax-free...
Modelling Linear Logic Without Units (Preliminary Results) (2005)
Houston, Robin, Hughes, Dominic, Schalk, Andrea
We describe a notion of categorical model for unitless fragments of (multiplicative) linear logic. The basic definition uses promonoidal categories, and we also give an equivalent elementary...
Classical Logic = Fibred MLL (2005)
This paper represents classical propositional proofs as *combinatorial proofs*, which are more abstract than proof nets: superposition (contraction/weakening) is modelled mathematically, as a lax...
Classical logic = MLL + Superposition (2005)
Syntactically, classical logic decomposes thus [Gir87]:
"[M]athematicians care no more for logic than logicians for mathematics." Augustus de Morgan, 1868. Proofs are traditionally syntactic, inductively generated objects. This paper presents an abstract...
Information hiding, anonymity and privacy: a modular approach (2004)
Dominic Hughes, Vitaly Shmatikov
SRI INTERNATIONAL We propose a new specification framework for information hiding properties such as anonymity and privacy. The framework is based on the concept of a function view, which is a...
Information hiding, anonymity and privacy: a modular approach (2004)
Dominic Hughes, Vitaly Shmatikový
SRI INTERNATIONAL We propose a new specification framework for information hiding properties such as anonymity and privacy. The framework is based on the concept of a function view, which is a...
Information hiding, anonymity and privacy: a modular approach (2004)
Dominic Hughes, Vitaly Shmatikov
SRI INTERNATIONAL We develop a new specification framework for security properties. The framework is based on the notion of a function view, which is a concise representation of partial information...
Proof Nets for Unit-free Multiplicative-Additive Linear Logic (2003)
Extended Dominic, Dominic Hughes, Rob Van Glabbeek
this paper we propose a new notion of MALL proof net (Section 2) which adheres faithfully to the original MLL # This paper appeared in Proceedings 18th Annual IEEE Symposium on Logic in Computer...
Proof Nets for Unit-free Multiplicative-Additive Linear Logic (2003)
Extended Dominic, Dominic Hughes, Rob Van Glabbeek
this paper we propose a new notion of MALL proof net (Section 2) which adheres faithfully to the original MLL theory: we provide a simple inductive translation of cut-free # A preliminary version of...
Proof Nets for Unit-free Multiplicative-Additive Linear Logic (2003)
A cornerstone of the theory of proof nets for unit-free multiplicative linear logic (MLL) is the abstract representation of cut-free proofs modulo inessential commutations of rules. The only known...
Full completeness of the multiplicative linear logic of Chu spaces (1999)
Devarajan, Harish, Hughes, Dominic, Plotkin, Gordon, Pratt, Vaughan
We prove full completeness of multiplicative linear logic (MLL) without MIX under the Chu interpretation. In particular we show that the cut-free proofs of MLL theorems are in a natural bijection...
Full completeness of the multiplicative linear logic of Chu spaces (1999)
Devarajan, Harish, Hughes, Dominic, Plotkin, Gordon, Pratt, Vaughan
We prove full completeness of multiplicative linear logic (MLL) without MIX under the Chu interpretation. In particular we show that the cut-free proofs of MLL theorems are in a natural bijection...
Full completeness of the multiplicative linear logic of Chu spaces
Harish Devarajan, Dominic Hughes, Gordon Plotkin, Vaughan Pratt
We prove full completeness of multiplicative linear logic (MLL) without MIX under the Chu interpretation. In particular we show that the cut-free proofs of MLL theorems are in a natural bijection...