Stéphane Gimenez

Research

Publications

S. Gimenez and D. Obwaller. Interaction Automata and the ia2d Interpreter (FSCD 2016)
We introduce interaction automata as a topological model of computation and present the conceptual plane interpreter ia2d. Interaction automata form a refinement of both interaction nets and cellular automata models that combine data deployment, memory management and structured computation mechanisms. Their local structure is inspired from pointer machines and allows an asynchronous spatial distribution of the computation. Our tool can be considered as a proof-of-concept piece of abstract hardware on which functional programs can be run in parallel.
S. Gimenez and G. Moser. The Complexity of Interaction (POPL 2016)
In this paper, we analyze the complexity of functional programs written in the interaction-net computation model, an asynchronous, parallel and confluent model that generalizes linear-logic proof nets. Employing user-defined sized and scheduled types, we certify concrete time, space and space–time complexity bounds for both sequential and parallel reductions of interaction-net programs by suitably assigning complexity potentials to typed nodes. The relevance of this approach is illustrated on archetypal programming examples. The provided analysis is precise, compositional and is, in theory, not restricted to particular complexity classes.
S. Gimenez and G. Moser. The Structure of Interaction (CSL 2013)
Interaction nets form a local and strongly confluent model of computation that is per se parallel. We introduce a Curry–Howard correspondence between well-formed interaction nets and a deep-inference deduction system based on linear logic. In particular, linear logic itself is easily expressed in the system and its computational aspects materialise though the correspondence. The system of interaction nets obtained is a typed variant of already well-known sharing graphs. Due to a strong confluence property, strong normalisation for this system follows from weak normalisation. The latter is obtained via an adaptation of Girard's reducibility method. The approach is modular, readily gives rise to generalisations (e.g. second order, known as polymorphism to the programmer) and could therefore be extended to various systems of interaction nets.
S. Gimenez. Realizability proof for normalization of Full Differential Linear Logic (TLCA 2011)
Realizability methods allowed to prove normalization results on many typed calculi. Girard adapted these methods to systems of nets and managed to prove normalization of second order Linear Logic. Our contribution is to provide an extension of this proof that embrace Full Differential Linear Logic (a logic that can describe both single-use resources and inexhaustible resources). Anchored within the realizability framework our proof is modular enough so that further extensions (to second order, to additive constructs or to any other independent feature that can be dealt with using realizability) come for free.

Thesis

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.