# ReACT Project (ended)

I submitted in September 2014 an application for a Marie Curie Individual Fellowship (call H2020-MSCA-IF-2014, Mathematics (MAT) Panel) which was successful. This project, ReACT (A Realizability Approach to Complexity Theory, grant agreement No 659920) funded a two-year research stay to work with Jakob Grue Simonsen at the Computer Science department of the University of Copenhagen (DIKU). It is part of the European Union's Horizon 2020 program for research and innovation. A (largely) expanded version of the associated research project, along with an exposition of first results, can be found in the preprint "Towards a Complexity-through-Realizability Theory".

## Documents

Here are links to (some) documents related to the project. Now that the project is over, this webpage will not be updated anymore even though some additional documents relating work done as part of the project may still be published in the future. Those will appear on the Research page anyway.

#### Publications (Journals)

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Nondeterministic Automata},

Journal = {ACM Transactions in Computational Logic},

Year = {2018},

Volume = {19},

Number = {3},

}

#### Publications (Conferences)

Author = {Aubert, Clément and Bagnol, Marc and Seiller, Thomas},

Chapter = {Unary Resolution: Characterizing Ptime},

Title = {Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings},

Year = {2016},

Publisher = {Springer Berlin Heidelberg},

Pages = {373--389},

Doi = {10.1007/978-3-662-49630-5_22},

}

*Geometry of Interaction*(GoI) constructions introduced so far. This series of work was inspired from Girard's hyperfinite GoI, and develops a quantitative approach that should be understood as a dynamic version of weighted relational models. Until now, the interaction graphs framework has been shown to deal with exponentials for the constrained system ELL (Elementary Linear Logic) while keeping its quantitative aspect. Adapting older constructions by Girard, one can clearly define "full" exponentials, but at the cost of these quantitative features. We show here that allowing interpretations of proofs to use continuous (yet finite in a measure-theoretic sense) sets of states, as opposed to earlier Interaction Graphs constructions were these sets of states were discrete (and finite), provides a model for full linear logic with second order quantification.

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Full Linear Logic},

Booktitle = {Logic in Computer Science (LICS)},

Year = {2016},

}

**Associated Tool/Software:**A prototype LLVM pass, and A Proof of Concept on C code.

In this paper, we introduce the theory around this concept and present a prototype analysis pass implemented on LLVM. We already implemented a proof of concept on a toy C parser3 analysing and transforming the AST representation. In a very near future, we will implement the corresponding transformation within our prototype LLVM pass and provide benchmarks comparisons.

Author = {Moyen, Jean-Yves and Rubiano, Thomas and Seiller, Thomas},

Title = {Loop Quasi-Invariant Chunk Detection},

Booktitle = {Automated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017, Pune, India, October 3--6, 2017, Proceedings},

Editor = {D’Souza, Deepak and Narayan Kumar, K.},

Pages = {91--108},

Year = {2017},

DOI = {10.1007/978-3-319-68167-2_7},

}

#### Tools/Software

#### Publications (Workshops)

**Associated Tool/Software:**A prototype LLVM pass, and A Proof of Concept on C code.

In this paper, we introduce the theory around this concept and present a proof-of-concept tool that we developed: an analysis and a transformation passes on a toy C parser written in Python called “pycparser” implemented by Eli Bendersky1. In the near future, we will implement these techniques on real compilers, as some of our optimisations are visibly better than current optimisations implemented in both GCC and LLVM.

Author = {Moyen, Jean-Yves and Rubiano, Thomas and Seiller, Thomas},

Title = {Loop Quasi-Invariant Chunk Motion by peeling with statement composition},

Editor = {Bonfante, Guillaume and Moser, Georg},

Year = {2017},

Booktitle = {{{\rm Proceedings 8th Workshop on} Developments in Implicit Computational complExity {\rm and 5th Workshop on} FOundational and Practical Aspects of Resource Analysis, {\rm Uppsala, Sweden, April 22-23, 2017}},

Series = {Electronic Proceedings in Theoretical Computer Science},

Volume = {248},

Publisher = {Open Publishing Association},

Pages = {47--59},

DOI = {10.4204/EPTCS.248.9},

}

#### Other Publications

Author = {Seiller, Thomas},

Title = {Why Complexity Theorists Should Care About Philosophy},

Booktitle = {Beyond Logic. Proceedings of the Conference held in Cerisy-la-Salle},

Editor = {Fichot, Jean and Piecha, Thomas},

Pages = {381--393},

Year = {2017},

DOI = {10.15496/publikation-18676},

}

#### Preprints and Research Reports

We analyse this original proof from a semantics point of view, interpreting programs as graphings -- generalizations of dynamical systems. We show that Mulmuley's method can be abstracted to a more general setting, exploiting the classic notion of topological entropy. This reformulation recentres the proof around dynamical aspects, relegating the use of algebraic geometry to a model-driven choice rather than a key concept of the method.

Author = {Pellissier, Luc and Seiller, Thomas},

Title = {Semantics, Entropy and Complexity Lower Bounds},

Note = {submitted},

Year = {2018},

}

We analyse this original proof from a semantics point of view, interpreting programs as graphings -- generalizations of dynamical systems. We show that Mulmuley's method can be abstracted to a more general setting, exploiting the classic notion of topological entropy. This reformulation recentres the proof around dynamical aspects, relegating the use of algebraic geometry to a model-driven choice rather than a key concept of the method.

Author = {Pellissier, Luc and Seiller, Thomas},

Title = {Entropy and Complexity Lower Bounds},

Note = {Abstract},

Year = {2018},

}

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Nondeterministic Automata},

Note = {submitted},

Year = {2016},

}

*geometry of interaction*-- and implicit computational complexity can lead to a new approach of computational complexity. This semantic-based approach should apply uniformly to various computational paradigms, and enable the use of new mathematical methods and tools to attack problem in computational complexity. This paper provides the background, motivations and perspectives of this

*complexity-through-realizability*theory to be developed, and illustrates it with recent results.

Author = {Seiller, Thomas},

Title = {Towards a Complexity-through-Realizability Theory},

Journal = {submitted},

Year = {2015},

}

Author = {Seiller, Thomas},

Title = {Measurable Preorders and Complexity},

Note = {Abstract},

Year = {2015},

}

Author = {Seiller, Thomas},

Title = {Interaction Graphs and Computational Complexity {I}},

Note = {in preparation},

Year = {2015},

}

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Zeta Functions},

Note = {in preparation},

Year = {2016},

}