Stéphane Gimenez



I did my PhD thesis (written in French) Programmer, calculer et raisonner avec les réseaux de la logique linéaire in the PPS laboratory in Paris, under Thomas Ehrhard's supervision.

The first part describes various systems of interaction nets (calculus using rewriting whose reduction is atomic, local and parallel) which simulate the execution of linear logic proofs (considered as programs). The different fragments of this logic are discussed, and a recursion construct is added to reach the expressiveness of common programming languages. The simulation method that was developed allows the execution of programs written in certain languages using a small multi-processor virtual machine. It relies on localized representations of boxes coming from proof nets; some of them advantageously use a control channel to avoid losing structure from the proofs they represent.

The second part is devoted to differential linear logic and its single-use resources. It presents a super-promotion which, unlike the usual promotion, preserves the original symmetry of this formalism. This construction is the logical counterpart of the replication which can be found in some process algebras. We managed to isolate one of its more primitive components, namely co-digging, which is responsible for their (still) uncontrolled dynamic. Super-promotion can be expressed in the syntax of λ-calculus with resources or in systems of nets. Sequentialization of the latter requires a specific presentation of logic, based on a calculus of structures, which might open some other perspectives. Realizability for differential systems and relational semantics for the various nets we consider are also discussed.

Workshop Publications
Towards Generic Inductive Constructions in Systems of Nets (WST 2013)
Some slides

Analysis of Parallel Complexity in Interaction Nets

2FC 2014, Vienna.

Reducibility proof for normalization of Full Differential Linear Logic

June 3, 2011 in Novi Sad. PPS Seminar, June 30, 2011 in Paris.

Using structures to fix (or improve) several systems of nets derived from Linear Logic

Collegium Logicum, March 1, 2011 at LIX, Palaiseau.

Proofs nets and their semantics expressed by local means

CHoCo Seminar, October 7, 2010 in ÉNS Lyon.

Ressources, promotion, et super-promotion (in French)

CHoCo Seminar, November 8, 2008 in ÉNS Lyon.