Papers on dialogue categories

1. Game semantics in string diagrams [pdf]

June 2006 - onwards

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.

2. Dialogue categories up to deformation [pdf]

June 2006 - onwards

In this paper, we introduce the notion of dialogue chirality, a relaxed notion of dialogue category defined as an adjunction between a monoidal category A and a monoidal category B equivalent to its opposite category Aop. The comparison between dialogue categories and dialogue chiralities is based on the construction of a 2-dimensional adjunction 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.

3. An algebraic presentation of dialogue categories

June 2006 - onwards

Available soon

4. 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.

5. A functorial bridge between proofs and knots

January 2009 - onwards

Available soon

Papers on resource modalities

1. Resource modalities in tensorial logic [pdf]

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.

2. An explicit formula for the free exponential modality
of linear logic [pdf]

Joint work with Nicolas Tabareau & Christine Tasson.
Mathematical Structures in Computer Science (2012)
To appear.

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]

May 2007

Very first talk on tensorial logic, given in Siena and dedicated to Jean-Yves Girard on the occasion of his 60th birthday.

String diagrams: a functorial semantics of proofs [one] [two]

July 2009

Two invited talks at the Hopf Algebra conference in Luxembourg.

Programming languages in string diagrams
[one] [two] [three] [four-side-A] [four-side-B] [five]

June 2011

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 Scottish Category Theory Seminar followed up by a talk at the weekly Semantics Seminar of the PPS lab.

A functorial bridge between proofs and knots [pdf][video]

December 2011

Invited talk at the Category and Physics 2011 meeting in Paris.