Papers on dialogue categories
June 2006 - June 2012
A dialogue category is a symmetric monoidal category equipped with a notion of tensorial negation. We establish that the free dialogue category is a category of dialogue games and total innocent strategies. The connection clarifies the algebraic and logical nature of dialogue games, and their intrinsic connection to linear continuations. The proof of the statement is based on an algebraic presentation of dialogue categories inspired by knot theory, and a difficult factorization theorem established by rewriting techniques.
June 2006 - June 2012
We introduce a two-sided version of dialogue categories – called dialogue chiralities – formulated as an adjunction between a monoidal category A and a monoidal category B equivalent to the opposite category of A. The two-sided formulation is compared to the original one-sided formulation of dialogue categories by exhibiting a 2-dimensional equivalence between a 2-category of dialogue categories and a 2-category of dialogue chiralities. The resulting coherence theorem clarifies in what sense every dialogue chirality may be strictified to an equivalent dialogue category.
June 2006 - September 2012
Every dialogue category comes equipped with a continuation monad defined by applying the negation functor twice. In this paper, we advocate that this double negation monad should be understood as part of a larger parametric monad (or a lax action) with parameter taken in the opposite of the dialogue category. This alternative point of view has one main conceptual benefit: it reveals that the strength of the continuation monad is the fragment of a more fundamental and symmetric structure --- provided by a distributivity law between the parametric continuation monad and the canonical action of the dialogue category over itself. The purpose of this work is to describe the formal properties of this parametric continuation monad and of its distributivity law.
June 2006 - September 2016
Tensorial logic is a primitive logic of tensor and negation which refines linear logic by relaxing the hypothesis that linear negation is involutive. Thanks to this mild modification, tensorial logic provides a type-theoretic account of game semantics where innocent strategies are portrayed as temporal refinements of traditional proof-nets in linear logic. In this paper, we study the algebraic and combinatorial structure of negation in a non-commutative variant of tensorial logic. The analysis is based on a 2-categorical account of dialogue categories, which unifies tensorial logic with linear logic, and discloses a primitive symmetry between proofs and anti-proofs. The micrological analysis of tensorial negation reveals that it can be decomposed into a series of more elementary components: an adjunction between the left and right negation functors ; a pair of linear distributivity laws which refines the linear distributivity law between tensor and cotensor in linear logic, and generates the Opponent and Proponent views of innocent strategies between dialogue games ; a pair of axiom and cut combinators adapted from linear logic ; an involutive change of frame reversing the point of view of Prover and of Denier on the logical dispute, and reversing the polarity of moves in the dialogue game associated to the tensorial formula.
5. A micrological study of helical negation [pdf in progress]
June 2006 - onwards
This paper is the second part of the micrological study of negation initiated in our companion paper. We have encountered there a discrepancy between left and right dialogue chiralities which we resolve here by introducing the notion of ambidextrous dialogue chirality. One main purpose of the paper is to disclose the topological nature of this logical notion. More specifically, we establish that an ambidextrous chirality is the same thing as a left chirality equipped with an helical structure on its tensorial negation. This topological insight enables us to conclude the project initiated in our companion paper, and to present ambidextrous chiralities in a purely combinatorial way.
6. Braided notions of dialogue categories [pdf in progress]
January 2009 - onwards
A dialogue category is a monoidal category equipped with an exponentiating object bot called its tensorial pole. In a dialogue category, every object x is thus equipped with a left negation x --o bot and a right negation bot o-- x. An important point of the definition is that the object x is not required to coincide with its double negation. Our main purpose in the present article is to formulate two non commutative notions of dialogue categories -- called cyclic and balanced dialogue categories. In particular, we show that the category of left H-modules of arbitrary dimension on a ribbon Hopf algebra H defines a balanced dialogue category Mod(H) whose tensorial pole~$\bot$ is the underlying field k. We explain how to recover from this basic observation the well-known fact that the full subcategory of finite dimensional left H-modules defines a ribbon category.
7. A functorial bridge between proofs and knots
January 2009 - onwards
Tensorial logic is a primitive logic of tensor and negation which refines linear logic by relaxing the hypothesis that tensorial negation $A\mapsto \lnot \, A$ is involutive. The resulting logic of linear continuations provides a proof-theoretic account of game semantics, where the formulas and proofs of the logic reflect univoquely dialogue games and innocent strategies. In the present paper, we introduce a topologically-aware version of tensorial logic, called ribbon tensorial logic. We associate to every proof of the logic a ribbon tangle which tracks the flow of tensorial negations inside the proof. The translation is functorial: it is performed by exhibiting a correspondence between the notion of dialogue category in proof theory and the notion of ribbon category in knot theory. Our main theorem is that the translation is faithful: two tensorial proofs are equal modulo commuting conversions if and only if the associated ribbon tangles are equal up to topological deformation. The ``proof-as-tangle'' theorem may be also understood as a coherence theorem for ribbon dialogue categories. By connecting in this functorial way tensorial logic and knot theory, we hope to investigate further the unexpected topological nature of proofs and programs, and of their dialogical interpretation in game semantics.
8. Parametric monads and enriched adjunctions [pdf in progress]
March 2012 - onwards
Starting from the particular case of the double negation monad in dialogue categories, we investigate what additional structure is required of an adjunction in order to give rise to a strong monad. The analysis leads to a purely combinatorial description of enriched functors, enriched natural transformations and enriched adjunctions between categorical modules.
January 2009 - March 2013
About ten years ago, Brian Day and Ross Street discovered a beautiful and unexpected connection between the notion of star-autonomous category in proof theory and the notion of Frobenius algebra in mathematical physics. The purpose of the present paper is to clarify the logical content of this connection by formulating a two-sided presentation of Frobenius algebras. The presentation is inspired by the idea that every logical dispute has two sides consisting of a Prover and of a Denier. This dialogical point of view leads us to a correspondence between dialogue categories and Frobenius pseudomonoids. The correspondence with dialogue categories refines Day and Street’s correspondence with star-autonomous categories in the same way as tensorial logic refines linear logic.
10. Tensorial logic meets cobordism
January 2009 - onwards
May - September 2013
We explain how to see the set of positions of a dialogue game as a coherence space in the sense of Girard or as a bistructure in the sense of Curien, Plotkin and Winskel. The coherence structure on the set of positions results from a Kripke translation of tensorial logic into linear logic extended with a necessity modality. The translation is done in such a way that every innocent strategy defines a clique or a configuration in the resulting space of positions. This leads us to study the notion of configuration designed by Curien, Plotkin and Winskel for general bistructures in the particular case of a bistructure associated to a dialogue game. We show that every such configuration may be seen as an interactive strategy equipped with a backward as well as a forward dynamics based on the interplay between the stable order and the extensional order. In that way, the category of bistructures is shown to include a full subcategory of games and coherent strategies of an interesting nature.
Papers on resource modalities
Joint work with Nicolas Tabareau.
Annals of Pure and Applied Logic (2009)
Volume 161, Issue 5, Pages 632-653.
The description of resources in game semantics has never achieved the simplicity and precision of linear logic, because of the misleading conception that linear logic is more primitive than game semantics. Here, we defend the opposite view, and thus advocate that game semantics is conceptually more primitive than linear logic. This revised point of view leads us to introduce tensor logic, a primitive variant of linear logic where negation is not involutive. After formulating its categorical semantics, we interpret tensor logic in a model based on Conway games equipped with a notion of payoff, in order to reflect the various resource policies of the logic: linear, affine, relevant or exponential.
Joint work with Nicolas Tabareau & Christine Tasson.
Mathematical Structures in Computer Science (2012)
The exponential modality of linear logic associates a commutative comonoid !A to every formula A, this enabling to duplicate the formula in the course of reasoning. Here, we explain how to compute the free commutative comonoid !A as a sequential limit of equalizers in any symmetric monoidal category where this sequential limit exists and commutes with the tensor product. We apply this general recipe to a series of models of linear logic, typically based on coherence spaces, Conway games and finiteness spaces. This algebraic description unifies for the first time the various constructions of the exponential modality in spaces and games. It also sheds light on the duplication policy of linear logic, and its interaction with classical duality and double negation completion.
A few talks
Towards an algebra of duality [pdf]
Very first talk on tensorial logic, given in Siena and dedicated to Jean-Yves Girard on the occasion of his 60th birthday.
Two invited talks at the Hopf Algebra conference in Luxembourg.
Programming languages in string diagrams
Five lectures at the Oregon Summer School on Programming Languages in Eugene.
Braided notions of dialogue categories [pdf]
November 2011 -- January 2012
Invited talk at the Category and Physics 2011 meeting in Paris.
Tensorial logic with algebraic effects [pdf]
Invited talk at the Proofs and Programs 2012 meeting in CIRM, Luminy.