22 citations · 40 across the 13 of their papers we have counts for
6 papers · 1 filter
Simple multiplicative proof nets with units
Dominic Hughes
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…
Simple free star-autonomous categories and full coherence
Dominic Hughes
This paper gives a simple presentation of the free star-autonomous category over a category, based on Eilenberg-Kelly-MacLane graphs and Trimble rewiring, yielding a full coherence…
A minimal classical sequent calculus free of structural rules
Dominic Hughes
Gentzen's classical sequent calculus LK has explicit structural rules for contraction and weakening. They can be absorbed (in a right-sided formulation) by replacing the axiom P,(n…
Logic Without Syntax
Dominic Hughes
This paper presents an abstract, mathematical formulation of classical propositional logic. It proceeds layer by layer: (1) abstract, syntax-free propositions; (2) abstract, syntax…
Modelling Linear Logic Without Units (Preliminary Results)
Robin Houston, Dominic Hughes, Andrea Schalk
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…
Classical Logic = Fibred MLL
Dominic Hughes
This paper represents classical propositional proofs as *combinatorial proofs*, which are more abstract than proof nets: superposition (contraction/weakening) is modelled mathemati…