(Sambo) Boris ENG.

Activity report, september 2020. LIPN (LoVe), Université Sorbonne Paris Nord.

I’m interested in simple questions such as what logic and computation are.

Current works

Transcendental Syntax for multiplicative linear logic. The Transcendental Syntax is a programme initiated by Jean-Yves Girard suggesting a reconstruction of linear logic from a new model of computation. This programme, following his “Geometry of Interaction” (GoI) programme, rely on 4 atypical, hyperbolic and cryptic articles. During my master 2 internship, I had to go through the understanding of the GoI and together with Thomas Seiller, we produced a naive formalisation of his first paper on the Transcendental Syntax. During the first year of my PhD thesis, we produced a more accurate and rigorous formalisation leading to the submission of the article “Stellar Resolution: Multiplicatives”. From computational objects, we are able to retrieve the notion of proof and formula/type within multiplicative linear logic.

Stellar Resolution. The stellar resolution, is an asynchronous model of computation introduced in the Transcendental Syntax programme of Jean-Yves Girard. This model, based on first-order term unification (actually Robinson’s resolution), shows a lot of similarities with other models such as Girard’s flows (mainly studied by Marc Bagnol) and self-assembling abstract tile assembly model (which can be seen as an extension of Wang’s tiles) used in DNA computing and bioinformatics. We have yet to understand the stellar resolution as a computational model (what is computable, termination analysis, connexions to other models or theories etc).

Space complexity of the lambda-calculus. While the question of complexity is clear for Turing machines (tape cells used and number of steps), it is way more subtle for the lambda-calculus which became in logic through the Curry-Howard correspondence. Damiano Mazza and I, following our introductory work during my master 1 internship, are trying to study the space complexity of the lambda-calculus by using methods from intersection types, boolean circuits and the Geometry of Interaction. We would like to show that the lambda-calculus is relatively close to Turing machines in term of complexity in order to provide alternative definition of space complexity classes.

Future works

Transcendental Syntax. I only worked on the Transcendental Syntax for the multiplicative fragment of linear logic. The full linear logic (+ second order) still has to be reconstructed from the stellar resolution (possibly extensions of it). More interestingly, Girard’s third article on the Transcendental Syntax describes a computational interpretation of first-order logic, something which has not be done yet in the Curry-Howard correspondence and it may potentially have applications to descriptive complexity.

Stellar Resolution and Implicit Computation Complexity. The model of stellar resolution generalises both Girard’s flows and Seiller’s interaction graphs. But both also have applications in Implicit Computational Complexity we can explore and retrive from our model. For instance, flows give a machine-independent characterisation of logarithmic space and polynomial time.

Static analysis and Implicit Computational Complexity. Following the works of Moyen, Rubiano and Seiller on the analysis of dependencies in static analysis and the works of Jones and Kristiansen in the complexity analysis of imperative programs, Thomas Seiller and Clément Aubert started a new project “StATyC” in which we are interested in the application of methods and tools from Implicit Computation Complexity and their application to the static analysis of compilers.