# Research

## Documents

#### Pre-Publications: Submitted

Finite semantics of polymorphism, complexity and the power of type fixpoints, with L.T.D. Nguyễn, P. Pistone and L. Tortora de Falco, 2019.

pdf

We introduce the notion of coherent graphs, and show how those can be used to define dynamic semantics for Multiplicative Linear Logic. The models thus obtained are finite with respect to several aspects (finite graphs, finite generation of types) and thus improve in this way previous constructions by Seiller. We also discuss how the added notion of coherence can also be used to introduce non-determinism.

@unpublished{seiller-FiniteMALL2,

Author = {Nguyễn, Lê Thành Dũng and Pistone, Paolo and Seiller, Thomas and Tortora de Falco, Lorenzo},

Title = {Finite semantics of polymorphism, complexity and the power of type fixpoints},

Note = {Submitted},

Year = {2019},

}

Author = {Nguyễn, Lê Thành Dũng and Pistone, Paolo and Seiller, Thomas and Tortora de Falco, Lorenzo},

Title = {Finite semantics of polymorphism, complexity and the power of type fixpoints},

Note = {Submitted},

Year = {2019},

}

PRAMs over integers do not compute maxflow efficiently, with L. Pellissier,

**last updated December 18th 2018**.
pdf

Finding lower bounds in complexity theory has proven to be an extremely difficult task. In this article, we analyze two proofs of complexity lower bound: Ben-Or's proof of minimal height of algebraic computational trees deciding certain problems and Mulmuley's proof that restricted Parallel Random Access Machines (PRAMs) over integers can not decide Ptime-complete problems efficiently. We present the aforementioned models of computation in a framework inspired by dynamical systems and models of linear logic : graphings.

This interpretation allows to connect the classical proofs to topological entropy, an invariant of these systems; to devise an algebraic formulation of parallelism of computational models; and finally to strengthen Mulmuley's result by separating the geometrical insights of the proof from the ones related to the computation and blending these with Ben-Or's proof. Looking forward, the interpretation of algebraic complexity theory as dynamical system might shed a new light on research programs such as Geometric Complexity Theory.

This interpretation allows to connect the classical proofs to topological entropy, an invariant of these systems; to devise an algebraic formulation of parallelism of computational models; and finally to strengthen Mulmuley's result by separating the geometrical insights of the proof from the ones related to the computation and blending these with Ben-Or's proof. Looking forward, the interpretation of algebraic complexity theory as dynamical system might shed a new light on research programs such as Geometric Complexity Theory.

@unpublished{seiller-PRAMsLB,

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

Title = {PRAMs over integers do not compute maxflow efficiently},

Note = {submitted},

Year = {2018},

}

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

Title = {PRAMs over integers do not compute maxflow efficiently},

Note = {submitted},

Year = {2018},

}

Coherent Interaction Graphs: A Non-Deterministic Geometry of Interaction for MLL, with L.T.D. Nguyễn, 2018.

pdf

We introduce the notion of coherent graphs, and show how those can be used to define dynamic semantics for Multiplicative Linear Logic. The models thus obtained are finite with respect to several aspects (finite graphs, finite generation of types) and thus improve in this way previous constructions by Seiller. We also discuss how the added notion of coherence can also be used to introduce non-determinism.

@unpublished{seiller-CohGraphs,

Author = {Nguyễn, Lê Thành Dũng and Seiller, Thomas},

Title = {Coherent Interaction Graphs: A Non-Deterministic Geometry of Interaction for MLL},

Note = {Submitted},

Year = {2018},

}

Author = {Nguyễn, Lê Thành Dũng and Seiller, Thomas},

Title = {Coherent Interaction Graphs: A Non-Deterministic Geometry of Interaction for MLL},

Note = {Submitted},

Year = {2018},

}

From Dynamic to Static Semantics, Quantitatively.

pdf

We exhibit a new relationship between dynamic and denotational semantics. We first define the categorical outlay needed to define Interaction Graphs models, a generalisation of Girard’s Geometry of Interaction models, which are strongly related to game semantics. We then show how this category is mapped to weighted relational models of linear logic. This brings into vision a new bridge between the dynamic and denotational approaches, and provides formal grounds for considering interaction graphs models as quantitative versions of GoI and game semantics models.

@unpublished{seiller-functorial,

Author = {Seiller, Thomas},

Title = {A functorial bridge between dynamic and denotational semantics},

Note = {Submitted},

Year = {2016},

}

Author = {Seiller, Thomas},

Title = {A functorial bridge between dynamic and denotational semantics},

Note = {Submitted},

Year = {2016},

}

Towards a Complexity-through-Realizability Theory.

pdf

We explain how recent developments in the fields of realizability models for linear logic -- or

*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.
@article{seiller-towards,

Author = {Seiller, Thomas},

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

Journal = {submitted},

Year = {2015},

}

Author = {Seiller, Thomas},

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

Journal = {submitted},

Year = {2015},

}

Interaction Graphs: Exponentials.

pdf

This paper tackles the complex issue of defining exponential connectives in the Interaction Graphs framework. In order to succeed in this, we use the notion of graphings, a generalization of graphs which was defined in earlier work. We explain how one can define a GoI model for Elementary Linear Logic (ELL) with second-order quantification, a sub-system of linear logic that captures the class of elementary time computable functions.

@article{seiller-IGExp,

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Exponentials},

Journal = {Logical Methods in Computer Science},

Year = {2016},

Note = {under revision},

}

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Exponentials},

Journal = {Logical Methods in Computer Science},

Year = {2016},

Note = {under revision},

}

#### Publications: Journals

Interaction Graphs: Nondeterministic Automata, ACM Transactions in Computational Logic 19(3), 2018.

This paper exhibits a series of semantic characterisations of sublinear nondeterministic complexity classes. These results fall into the general domain of logic-based approaches to complexity theory and so-called implicit computational complexity (ICC), i.e. descriptions of complexity classes without reference to specific machine models. In particular, it relates strongly to ICC results based on linear logic since the semantic framework considered stems from work on the latter. Moreover, the obtained characterisations are of a geometric nature: each class is characterised by a specific action of a group by measure-preserving maps.

@article{seiller-IGNDA,

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Nondeterministic Automata},

Journal = {ACM Transactions in Computational Logic},

Year = {2018},

Volume = {19},

Number = {3},

}

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Nondeterministic Automata},

Journal = {ACM Transactions in Computational Logic},

Year = {2018},

Volume = {19},

Number = {3},

}

A Correspondence between Maximal Abelian Sub-Algebras and Linear Logic Fragments, Mathematical Structures in Computer Science 28(1), 2018

This papers exhibits a correspondence between a classification of maximal abelian sub-algebras (MASAs) proposed by Jacques Dixmier and fragments of linear logic. We expose for this purpose a modified construction of Girard's hyperfinite geometry of interaction which interprets proofs as operators in a von Neumann algebra. The expressivity of the logic soundly interpreted in this model is dependent on properties of a MASA which is a parameter of the interpretation.

@article{seiller-masas,

Author = {Seiller, Thomas},

Title = {A Correspondence between Maximal Abelian Sub-Algebras and Linear Logic Fragments},

Journal = {Mathematical Structures in Computer Science},

Volume = {28},

Number = {1},

Pages = {77-139},

Year = {2018},

}

Author = {Seiller, Thomas},

Title = {A Correspondence between Maximal Abelian Sub-Algebras and Linear Logic Fragments},

Journal = {Mathematical Structures in Computer Science},

Volume = {28},

Number = {1},

Pages = {77-139},

Year = {2018},

}

An Intentionally Fully-Abstract Sheaf Model For π (Extended Version), with Clovis Eberhart and Tom Hirschowitz. Logical Methods in Computer Science 13(4), 2017.

Following previous work on CCS, we propose a compositional model for
the pi-calculus in which processes are interpreted as sheaves on
certain simple sites. We define an analogue of fair testing
equivalence in the model and show that our interpretation is
intensionally fully abstract for it. That is, the interpretation
preserves and reflects fair testing equivalence; and furthermore,
any strategy is fair testing equivalent to the interpretation of
some process. The central part of our work is the construction of
our sites, whose heart is a combinatorial presentation of
pi-calculus traces in the spirit of string diagrams. As in previous
work, the sheaf condition is analogous to innocence in
Hyland-Ong/Nickau games.

@article{seiller-pilayground,

Author = {Eberhart, Clovis and Hirschowitz, Tom and Seiller, Thomas},

Title = {An Intentionally Fully-Abstract Sheaf Model For π (Extended Version)},

Journal = {Logical Methods in Computer Science},

Year = {2017},

Volume = {13},

Number = {4},

}

Author = {Eberhart, Clovis and Hirschowitz, Tom and Seiller, Thomas},

Title = {An Intentionally Fully-Abstract Sheaf Model For π (Extended Version)},

Journal = {Logical Methods in Computer Science},

Year = {2017},

Volume = {13},

Number = {4},

}

Interaction Graphs: Graphings, Annals of Pure and Applied Logic 168 (2017), pp. 278–320.

This paper extends the approach developed in previous papers on Interaction Graphs by considering a generalization of graphs named graphings, which is in some way a geometric realization of a graph. This very general framework leads to a number of new models of multiplicative-additive linear logic which generalize Girard's geometry of interaction models and opens several new lines of research in computational complexity and quantum computation.

@article{seiller-IGGraphings,

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Graphings},

Journal = {Annals of Pure and Applied Logic},

Year = {2017},

Volume = {168},

Number = {2},

Month = {February},

Pages = {278--320},

}

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Graphings},

Journal = {Annals of Pure and Applied Logic},

Year = {2017},

Volume = {168},

Number = {2},

Month = {February},

Pages = {278--320},

}

Logarithmic Space and Permutations, with C. Aubert. Information and Computation 248 (2016), pp. 2–21.

In a previous paper, the authors showed how Girard proposal succeeds in obtaining a new characterization of co-NL languages as a set of operators acting on a Hilbert Space. In this paper, we extend this work by showing that it is also possible to define a set of operators characterizing the class L of deterministic logarithmic space languages.

@article{seiller-lsp,

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

Title = {Logarithmic Space and Permutations},

Journal = {Information and Computation},

Volume = {248},

Pages = {2--21},

Year = {2016},

DOI = {10.1016/j.ic.2014.01.018},

}

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

Title = {Logarithmic Space and Permutations},

Journal = {Information and Computation},

Volume = {248},

Pages = {2--21},

Year = {2016},

DOI = {10.1016/j.ic.2014.01.018},

}

Characterizing co-NL by a group action, with C. Aubert. Mathematical Structures in Computer Science 26 (2016), pp. 606—638.

In a previous paper, Girard proposed to use his recent construction of a geometry of interaction in the hyperfinite factor in an innovative way to characterize complexity classes. This work provides a complete proof that the complexity class co-NL can be characterized using this new approach. We introduce as a technical tool the non-deterministic pointer machine, a concrete model to computes algorithms in logarithmic space.

@article{seiller-conl,

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

Title = {Characterizing co-NL by a group action},

Journal = {Mathematical Structures in Computer Science},

Year = {2016},

Volume = {26},

Number = {4},

Pages = {606--638},

DOI = {10.1017/S0960129514000267},

}

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

Title = {Characterizing co-NL by a group action},

Journal = {Mathematical Structures in Computer Science},

Year = {2016},

Volume = {26},

Number = {4},

Pages = {606--638},

DOI = {10.1017/S0960129514000267},

}

Interaction Graphs: Additives, Annals of Pure and Applied Logic 167 (2016), pp. 95-154.

This paper presents a parametrized construction of a Geometry of Interaction model (GoI model) for Multiplicative Additive Linear Logic (MALL). Contrarily to former constructions dealing with additive connectives, we are able to solve here the known issue of obtaining a denotational semantics for MALL by introducing a notion of observational equivalence. This work is shown to generalize all previously considered GoI models and pinpoints an essential property, named the trefoil property, which underlies them.

@article{seiller-igadd,

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Additives},

Journal = {Annals of Pure and Applied Logic},

Volume = {167},

Number = {2},

Year = {2016},

Pages = {95 -- 154},

Issn = {0168-0072},

Publisher = {Elsevier Science Publishers Ltd.},

Doi = {http://dx.doi.org/10.1016/j.apal.2015.10.001},

}

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Additives},

Journal = {Annals of Pure and Applied Logic},

Volume = {167},

Number = {2},

Year = {2016},

Pages = {95 -- 154},

Issn = {0168-0072},

Publisher = {Elsevier Science Publishers Ltd.},

Doi = {http://dx.doi.org/10.1016/j.apal.2015.10.001},

}

Interaction Graphs: Multiplicatives, Annals of Pure and Applied Logic 163 (2012), pp. 1808-1837.

This paper defines a combinatorial approach to J.-Y. Girard's geometry of interaction in the hyperfinite factor, replacing operator-algebraic notion by usual graph-theoretical notions. In particular, it is shown that the Fuglede-Kadison determinant in the type II$_1$ hyperfinite factor can be computed as a measure of the sets of cycles in a graph.

@article{seiller-igmult,

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Multiplicatives},

Journal = {Annals of Pure and Applied Logic},

Volume = {163},

Year = {2012},

Month = {December},

Pages = {1808-1837},

Publisher = {Elsevier Science Publishers Ltd.},

Doi = {http://dx.doi.org/10.1016/j.apal.2012.04.005},

}

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Multiplicatives},

Journal = {Annals of Pure and Applied Logic},

Volume = {163},

Year = {2012},

Month = {December},

Pages = {1808-1837},

Publisher = {Elsevier Science Publishers Ltd.},

Doi = {http://dx.doi.org/10.1016/j.apal.2012.04.005},

}

#### Publications: Conferences

Loop Quasi-Invariant Chunk Detection, with J.-Y. Moyen and T. Rubiano, ATVA 2017.

**Associated Tool/Software:**A prototype LLVM pass, and A Proof of Concept on C code.Several techniques for analysis and transformations are used in compilers. Among them, the peeling of loops for hoisting quasi-invariants can be used to optimize generated code, or simply ease developers’ lives. In this paper, we introduce a new concept of dependency analysis borrowed from the field of Implicit Computational Complexity (ICC), allowing to work with composed statements called “Chunks” to detect more quasi-invariants. Based on an optimization idea given on a WHILE language, we provide a transformation method - reusing ICC concepts and techniques - to compilers. This new analysis computes an invariance degree for each statement or chunks of statements by building a new kind of dependency graph, finds the “maximum” or “worst” dependency graph for loops, and recognizes if an entire block is Quasi-Invariant or not. This block could be an inner loop, and in that case the computational complexity of the overall program can be decreased.

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.

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.

@inproceedings{seiller-ATVA,

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},

}

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},

}

Interaction Graphs: Full Linear Logic, LICS 2016.

Interaction graphs were introduced as a general, uniform, construction of dynamic models of linear logic, encompassing all

*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.
@inproceedings{seiller-IGFull,

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Full Linear Logic},

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

Year = {2016},

}

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Full Linear Logic},

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

Year = {2016},

}

Unary Resolution: Characterizing Ptime, with Marc Bagnol and Clément Aubert, FOSSACS 2016.

pdf

We give a characterization of deterministic polynomial time computation based on an algebraic structure called the resolution semiring (whose elements can be understood as logic programs or sets of rewriting rules over first-order terms), a construction stemming from an interactive interpretation of cut-elimination known as the geometry of interaction. More precisely, we restrict this framework to terms (logic programs, rewriting rules) using only unary symbols. We prove it is complete for polynomial time computation using an encoding of pushdown automata. Soundness w.r.t. Ptime is proven thanks to a saturation method close to pushdown systems and memoization.
As a direct consequence, we get a Ptime-completeness result for a class of logic programming queries that uses only unary function symbols.

@inbook{seiller-ptime,

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},

}

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},

}

An intensionally fully-abstract sheaf model for π, with Clovis Eberhart and Tom Hirschowitz. CALCO 2015. Best paper award.

Following previous work on CCS, we propose a compositional model for
the pi-calculus in which processes are interpreted as sheaves on
certain simple sites. We define an analogue of fair testing
equivalence in the model and show that our interpretation is
intensionally fully abstract for it. That is, the interpretation
preserves and reflects fair testing equivalence; and furthermore,
any strategy is fair testing equivalent to the interpretation of
some process. The central part of our work is the construction of
our sites, whose heart is a combinatorial presentation of
pi-calculus traces in the spirit of string diagrams. As in previous
work, the sheaf condition is analogous to innocence in
Hyland-Ong/Nickau games.

@inproceedings{seiller-picalco,

Author = {Eberhart, Clovis and Hirschowitz, Tom and Seiller, Thomas},

Title = {An Intensionally Fully-abstract Sheaf Model for $\pi$},

Booktitle = {6th Conference on Algebra and Coalgebra in Computer Science, {CALCO} 2015, June 24-26, 2015, Nijmegen, The Netherlands},

Editor = {Moss, Laurence and Sobocinski, Pawel},

Publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},

Pages = {86-100},

Year = {2015},

Doi = {10.4230/LIPIcs.CALCO.2015.86},

}

Author = {Eberhart, Clovis and Hirschowitz, Tom and Seiller, Thomas},

Title = {An Intensionally Fully-abstract Sheaf Model for $\pi$},

Booktitle = {6th Conference on Algebra and Coalgebra in Computer Science, {CALCO} 2015, June 24-26, 2015, Nijmegen, The Netherlands},

Editor = {Moss, Laurence and Sobocinski, Pawel},

Publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},

Pages = {86-100},

Year = {2015},

Doi = {10.4230/LIPIcs.CALCO.2015.86},

}

Logic Programming and Logarithmic Space, with C. Aubert, M. Bagnol and P. Pistone. APLAS 2014.

This paper presents an algebraic view on logic programming, related to proof theory and more specifically linear logic and geometry of interaction. Within this construction, a characterization of logspace (deterministic and non-deterministic) computation is given via a synctactic restriction, using an encoding of words that derives from proof theory.

@inproceedings{seiller-lpls,

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

Title = {Logic Programming and Logarithmic Space},

Pages = {39--57},

Doi = {10.1007/978-3-319-12736-1_3},

Editor = {Jacques Garrigue},

Booktitle = {Programming Languages and Systems - 12th Asian Symposium, {APLAS} 2014, Singapore, November 17-19, 2014, Proceedings},

Series = {Lecture Notes in Computer Science},

Volume = {8858},

Publisher = {Springer},

Year = {2014},

}

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

Title = {Logic Programming and Logarithmic Space},

Pages = {39--57},

Doi = {10.1007/978-3-319-12736-1_3},

Editor = {Jacques Garrigue},

Booktitle = {Programming Languages and Systems - 12th Asian Symposium, {APLAS} 2014, Singapore, November 17-19, 2014, Proceedings},

Series = {Lecture Notes in Computer Science},

Volume = {8858},

Publisher = {Springer},

Year = {2014},

}

#### Publications: Book Chapters (Peer Reviewed)

Verificationism and classical realizability, with Alberto Naibo and Mattia Petrolo.

*In*C. Baskent (Ed.) Perspectives on Interrogative Models of Inquiry (Springer).A comparison between intuitionistic realizability à la Kleene and classical realizability à la Krivine is provided. It is shown that while in the former the existence of realizers which are not proofs leads to the realization of non-provable sentences, in the latter the existence of realizers that are not proofs does not create any kind of asymmetry between the set of realized sentences and that of proved ones. The existence of such realizers is needed instead for giving a computational interpretation of classical proofs. In this way classical realizability can be used as a framework for an anti-realist account of classical logic. Moreover, this account is shown to be compatible with a single-agent verificationist position, that is without passing through the standard game-theoretic interpretations involving (at least) two players.

@inbook{seiller-vcr,

Author = {Naibo, Alberto and Petrolo, Mattia and Seiller, Thomas},

Title = {Verificationism and classical realizability},

DOI = {10.1007/978-3-319-20762-9_9},

Booktitle = {Perspectives on Interrogative Models of Inquiry},

Editors = {Baskent, Can},

Series = {Logic, Argumentation & Reasoning},

Publisher = {Springer},

Year = {2015},

}

Author = {Naibo, Alberto and Petrolo, Mattia and Seiller, Thomas},

Title = {Verificationism and classical realizability},

DOI = {10.1007/978-3-319-20762-9_9},

Booktitle = {Perspectives on Interrogative Models of Inquiry},

Editors = {Baskent, Can},

Series = {Logic, Argumentation & Reasoning},

Publisher = {Springer},

Year = {2015},

}

On the Computational Meaning of Axioms, with Alberto Naibo and Mattia Petrolo.

*In*O. Pombo, A. Nepomuceno, J. Redmond (Edsmathe.) Epistemology, Knowledge and the Impact of Interaction (Springer).
pdf

An anti-realist theory of meaning suitable for both logical and proper axioms is investigated. As opposed to other anti-realist accounts, like Dummett-Prawitz verificationism, the standard framework of classical logic is not called into question. In particular, semantical features are not limited solely to inferential ones, but also computational aspects play an essential role in the process of determination of meaning. In order to deal with such computational aspects, a relaxation of syntax is shown to be necessary. This leads to a general kind of proof theory, where the objects of study are not typed objects like deductions, but rather untyped ones, in which formulas have been replaced by geometrical configurations.

@inbook{seiller-axioms,

Author = {Naibo, Alberto and Petrolo, Mattia and Seiller, Thomas},

Title = {On the Computational Meaning of Axioms},

Booktitle = {Epistemology, Knowledge and the Impact of Interaction},

Editors = {Pombo Martins, Olga and Nepomuceno Fernandez, Angel and Redmond, Juan},

Publisher = {Springer},

Series = {Logic, Epistemology, and the Unity of Science},

Volume = {38},

Pages = {141—184},

Year = {2016},

DOI = {10.1007/978-3-319-26506-3_5},

}

Author = {Naibo, Alberto and Petrolo, Mattia and Seiller, Thomas},

Title = {On the Computational Meaning of Axioms},

Booktitle = {Epistemology, Knowledge and the Impact of Interaction},

Editors = {Pombo Martins, Olga and Nepomuceno Fernandez, Angel and Redmond, Juan},

Publisher = {Springer},

Series = {Logic, Epistemology, and the Unity of Science},

Volume = {38},

Pages = {141—184},

Year = {2016},

DOI = {10.1007/978-3-319-26506-3_5},

}

#### Publications: Workshops

Loop Quasi-Invariant Chunk Motion by peeling with statement composition, with J.-Y. Moyen and T. Rubiano, DICE-FOPARA 2017.

**Associated Tool/Software:**A prototype LLVM pass, and A Proof of Concept on C code.Several techniques for analysis and transformations are present and used since the creation of compilers. Among them, the peeling of loops for hoisting quasi-invariants can be used to optimize generated code, or simply ease developers’ lives. In this paper, we introduce a new concept of dependency analysis borrowed from the field of Implicit Computational Complexity (ICC), allowing to work with composed statements called “Chunks” to detect more quasi- invariants. From a proven optimization idea given on a WHILE language, we provide a transformation method - reusing ICC concepts and techniques - to compilers. This new analysis computes an invariance degree for each statement or chunks of statements by building a new kind of dependency graph, finds the “maximum” or “worst” dependency graph for loops, and recognizes if an en- tire block is Quasi-Invariant or not. This block could be an inner loop, and in that case the computational complexity of the overall program can be decreased.

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.

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.

@unpublished{seiller-peeling,

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},

}

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},

}

#### Tools/Software

A prototype LLVM pass, https://github.com/ThomasRuby/lqicm_pass, implementing the loop optimisation described in the series of joint papers with J.-Y. Moyen and T. Rubiano.

A proof-of-concept in python for optimising C programs, https://github.com/ThomasRuby/LQICM_On_C_Toy_Parser, implementing the loop optimisation described in the series of joint papers with J.-Y. Moyen and T. Rubiano.

#### Publications: Others

Recension de "The blind spot. Lectures on logic" par J.-Y. Girard., with Christian Rétoré. Gazette des Mathématiciens 142 (pp. 136-143).

pdf

This is a short review (in french) of J.-Y. Girard's book "The blind spot. Lectures on logic" (European Mathematical Society 2011).

@article{seiller-recension,

Author = {Retor{\'e}, Christian and Seiller, Thomas},

Title = {Recension de" The blind spot. Lectures on logic" par J.-Y. Girard (European Mathematical Society, 2011).},

Journal = {La gazette des math{\'e}maticiens},

Volume = {142},

Pages = {136--143},

Year = {2014},

Month = {October},

}

Author = {Retor{\'e}, Christian and Seiller, Thomas},

Title = {Recension de" The blind spot. Lectures on logic" par J.-Y. Girard (European Mathematical Society, 2011).},

Journal = {La gazette des math{\'e}maticiens},

Volume = {142},

Pages = {136--143},

Year = {2014},

Month = {October},

}

Why Complexity Theorists Should Care About Philosophy. Jean Fichot, Thomas Piecha (editors), Beyond Logic. Proceedings of the Conference held in Cerisy-la-Salle, pp. 381--393.

Invited Talk at the ANR-DFG Beyond Logic conference.

@inproceedings{seiller-recension,

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},

}

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},

}

#### Pre-Publications: In preparation

Interaction Graphs and Computational Complexity I, in preparation.

(Draft)

The aim of Implicit Computational Complexity is to study algorithmic complexity only in terms of restrictions of languages and computational principles. Based on previous work about realizability models for linear logic, we propose a new approach where we consider semantical restrictions instead of syntactical ones. This leads to a hierarchy of models mirroring subtle distinctions about computational principles. As an illustration of the method, we explain how to obtain characterizations of infinite families of complexity classes lying in between the set of regular languages (resp. stochastic languages) and the sets of (deterministic and non-deterministic) logarithmic space predicates (resp. probabilistic logarithmic space predicates).

@unpublished{seiller-IGCompI,

Author = {Seiller, Thomas},

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

Note = {in preparation},

}

Author = {Seiller, Thomas},

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

Note = {in preparation},

}

Logical Constants from a Computational Point of View, with Alberto Naibo and Mattia Petrolo, in preparation.

The topic of this paper is the problem of characterizing the meaning of logical constants. Our proposal stands in the line of proof-theoretic semantics, exploiting in an essential way the proofs-as-programs correspondence. We first present the inferentialist position in order to point out some of its problems. Their analysis and solutions are carried out in the light of the Curry-Howard correspondence. It is on this basis that we can formulate a necessary condition for logicality, which naturally emerges from the computational point of view adopted here.

@unpublished{seiller-LogConst,

Author = {Naibo, Alberto and Petrolo, Mattia and Seiller, Thomas},

Title = {Logical Constants from a Computational Point of View},

Note = {in preparation},

}

Author = {Naibo, Alberto and Petrolo, Mattia and Seiller, Thomas},

Title = {Logical Constants from a Computational Point of View},

Note = {in preparation},

}

Interaction Graphs: Pure Lambda-Calculi, in preparation.

@unpublished{seiller-IGPure,

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Pure Lambda-Calculi},

Note = {in preparation},

}

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Pure Lambda-Calculi},

Note = {in preparation},

}

Interaction Graphs: Zeta Functions, in preparation.

@unpublished{seiller-IGZeta,

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Zeta Functions},

Note = {in preparation},

}

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Zeta Functions},

Note = {in preparation},

}

#### Other Documents: Workshops, Technical Reports

A semantic conjecture on second-order MLL and its complexity consequences (work in progress), Abstract for Linearity-TLLA 2018.

pdf

Semantic evaluation has proven to be a valuable tool to prove computational complexity results on monomorphic type systems. Can we apply it in presence of impredicative polymorphism? The linearity and stratification at work in light logics might make it possible.

@unpublished{seiller-SemConj,

Author = {Nguyễn, Lê Thành Dũng and Seiller, Thomas},

Title = {A semantic conjecture on second-order MLL and its complexity consequences (work in progress)},

Note = {Abstract (Linearity-TLLA 2018)},

Year = {2018},

}

Author = {Nguyễn, Lê Thành Dũng and Seiller, Thomas},

Title = {A semantic conjecture on second-order MLL and its complexity consequences (work in progress)},

Note = {Abstract (Linearity-TLLA 2018)},

Year = {2018},

}

Coherent Interaction Graphs: A Non-Deterministic Geometry of Interaction for MLL, Abstract for Linearity-TLLA 2018.

pdf

We introduce the notion of coherent graphs, and show how those can be used to define dynamic semantics for Multiplicative Linear Logic. The models thus obtained are finite with respect to several aspects (finite graphs, finite generation of types) and thus improve in this way previous constructions by Seiller. We also discuss how the added notion of coherence can also be used to introduce non-determinism.

@unpublished{seiller-CohGraphsAbs,

Author = {Nguyễn, Lê Thành Dũng and Seiller, Thomas},

Title = {Coherent Interaction Graphs: A Non-Deterministic Geometry of Interaction for MLL},

Note = {Abstract (Linearity-TLLA 2018)},

Year = {2018},

}

Author = {Nguyễn, Lê Thành Dũng and Seiller, Thomas},

Title = {Coherent Interaction Graphs: A Non-Deterministic Geometry of Interaction for MLL},

Note = {Abstract (Linearity-TLLA 2018)},

Year = {2018},

}

Entropy and Complexity Lower Bounds, Abstract for Linearity-TLLA 2018.

pdf

Finding lower bounds in complexity theory has proven to be an extremely difficult task. Nowadays, only one research direction is commonly acknowledged to have the ability to solve current open problems, namely Mulmuley's Geometric Complexity Theory programme. Relying on heavy techniques from algebraic geometry, it stemmed from a first lower bound result for a variant of Parallel Random Access Machines.

We analyse this original proof, together with two other proofs of lower bounds from a semantics point of view, interpreting programs as graphings -- generalizations of dynamical systems. We show that, abstracted to a more general setting that exploits the classic notion of topological entropy, this three proofs share the same structure. This reformulation recentres the proofs around dynamical aspects, relegating the use of algebraic geometry to a model-driven choice rather than a key concept of the method.

We analyse this original proof, together with two other proofs of lower bounds from a semantics point of view, interpreting programs as graphings -- generalizations of dynamical systems. We show that, abstracted to a more general setting that exploits the classic notion of topological entropy, this three proofs share the same structure. This reformulation recentres the proofs around dynamical aspects, relegating the use of algebraic geometry to a model-driven choice rather than a key concept of the method.

@unpublished{seiller-SECLBlin,

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

Title = {Entropy and Complexity Lower Bounds},

Note = {Abstract (Linearity-TLLA 2018)},

Year = {2018},

}

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

Title = {Entropy and Complexity Lower Bounds},

Note = {Abstract (Linearity-TLLA 2018)},

Year = {2018},

}

Entropy and Complexity Lower Bounds, Abstract for DICE 2018.

pdf

Finding lower bounds in complexity theory has proven to be an extremely difficult task. Nowadays, only one research direction is commonly acknowledged to have the ability to solve current open problems, namely Mulmuley's Geometric Complexity Theory programme. Relying on heavy techniques from algebraic geometry, the latter stemmed from a first lower bound result for a variant of Parallel Random Access Machines (PRAMs).

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.

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.

@unpublished{seiller-SECLBabs,

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

Title = {Entropy and Complexity Lower Bounds},

Note = {Abstract (DICE 2018)},

Year = {2018},

}

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

Title = {Entropy and Complexity Lower Bounds},

Note = {Abstract (DICE 2018)},

Year = {2018},

}

Semantics, Entropy and Complexity Lower Bounds, with L. Pellissier.

pdf

Finding lower bounds in complexity theory has proven to be an extremely difficult task. Nowadays, only one research direction is commonly acknowledged to have the ability to solve current open problems, namely Mulmuley's Geometric Complexity Theory programme. Relying on heavy techniques from algebraic geometry, the latter stemmed from a first lower bound result for a variant of Parallel Random Access Machines (PRAMs).

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.

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.

@unpublished{seiller-SECLB,

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

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

Note = {Technical Report},

Year = {2018},

}

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

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

Note = {Technical Report},

Year = {2018},

}

Interaction Graphs and Quantitative Semantics, Abstract for GaLoP 2016.

pdf

Interaction Graphs models were introduced as a generalisation of Girard's Geometry of Interaction constructions based on the interpretation of proofs as (finite, weigthed) graphs. Recent results use these models to bring into vision a new relation between dynamic and denotational semantics, providing formal grounds to the claim that Interaction Graphs models can be understood as a quantitative generalisation of dynamic semantics.

@unpublished{seiller-galop16,

Author = {Seiller, Thomas},

Title = {Interaction Graphs and Quantitative Semantics},

Note = {Abstract for GaLoP},

Year = {2016},

}

Author = {Seiller, Thomas},

Title = {Interaction Graphs and Quantitative Semantics},

Note = {Abstract for GaLoP},

Year = {2016},

}

Measurable Preorders and Complexity, Abstract for TACL 2015.

pdf

In a recent paper, we defined a generic construction of models of the exponential-free fragment of Linear Logic (MALL). These models provide a new framework for the study of computational complexity which allows for the use of techniques and invariants form ergodic theory and operator theory.

@journal{seiller-tacl2015,

Author = {Seiller, Thomas},

Title = {Measurable Preorders and Complexity},

Year = {2015},

Note = {Abstract for TACL},

}

Author = {Seiller, Thomas},

Title = {Measurable Preorders and Complexity},

Year = {2015},

Note = {Abstract for TACL},

}

Memoization for Unary Logic Programming: Characterizing Ptime, Research report. Joint work with Marc Bagnol and Clément Aubert, January 2015.

pdf

This paper provides a new characterization of deterministic polynomial time computation via a semiring based on the resolution rule, an algebraic structure originally introduced to build interactive models of linear logic. We study a specific sub-semiring restricted to unary symbols and show it is expressive enough to represent the computation of a type of pushdown automata that are known to correspond to deterministic polynomial time computation. Moreover, we show that acceptance by observations (the counterpart of a program in our construction) based on this sub-semiring can be decided in polynomial time, using an adaptation of the memoization technique to our algebraic context.

@unpublished{seiller-memoization,

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

Title = {Memoization for Unary Logic Programming: Characterizing Ptime},

Note = {https://hal.archives-ouvertes.fr/hal-01107377},

Year = {2015},

}

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

Title = {Memoization for Unary Logic Programming: Characterizing Ptime},

Note = {https://hal.archives-ouvertes.fr/hal-01107377},

Year = {2015},

}

Interaction Graphs and Complexity, Abstract.

pdf

The aim of Implicit Computational Complexity is to study algorithmic complexity only in terms of restrictions of languages and computational principles. Based on previous work about realizability models for linear logic, we propose a new approach where we consider semantical restrictions instead of syntactical ones. This leads to a hierarchy of models mirroring subtle distinctions about computational principles. As an illustration of the method, we explain how to obtain characterizations of the set of regular languages and the set of logarithmic space predicates.

@unpublished{seiller-igcomp,

Author = {Seiller, Thomas},

Title = {Interaction Graphs and Complexity},

Note = {Abstract},

Year = {2014},

}

Author = {Seiller, Thomas},

Title = {Interaction Graphs and Complexity},

Note = {Abstract},

Year = {2014},

}

Logarithmic Space and Permutations, Abstract for DICE 2013.

pdf

In a recent work, Girard proposed a new and innovative approach to computational complexity based on the proofs-as-programs correspondence. The authors recently showed how Girard proposal succeeds in obtaining characterizations of L and co-NL languages as sets of operators in the hyperfinite factor of type II$_{1}$.

@unpublished{seiller-dice2013,

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

Title = {Logarithmic Space and Permutations (Abstract)},

Note = {Abstract},

Year = {2013},

}

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

Title = {Logarithmic Space and Permutations (Abstract)},

Note = {Abstract},

Year = {2013},

}

#### Other Documents: Slides

A geometric theory of computational complexity. Thirty Years of Linear Logic conference, Rome, Italy, October 25th, 2017. pdf

Why Complexity Theorists Should Care About Philosophy, ANR-DFG BeyondLogic Conference, Cerisy-la-Salle, May 2017pdf

Computational Complexity, between Algebra and Geometry, GEOCAL-LAC meeting, November 2016pdf

A realisability approach to complexity theory, HCC seminar, November 27th 2015, University of Copenhagen (Denmark)pdf

Measurable Preorders and Complexity, TACL2015, June 26th 2015, Ischia Porto (IT)pdf

Towards a Complexity-through-Realizability Theory, FOPARA/DICE, ETAPS Workshop, April 12th 2015, London (UK)pdf

Geometry of Interaction: Old and New, Oberseminar Logik und Sprachtheorie, Tübingen, October 29th 2013pdf

Geometry of Interaction (part I), International Summer School on Linear Logic and Geometry of Interaction, Turin (Italy), August 27th-31st, 2013pdf

The Geometry of Interaction Program, 68nqrt seminar, IRISA/INRIA Rennes, June 13th 2013pdf

Logarithmic Space and Permutations, Workshop DICE (Developments in Implicit Computational complExity, March 17th 2013, Romepdf

Interaction Graphs: Exponentials, Talk given at February 1st 2013 LOGOI Meeting, Marseillepdf

From Proof Nets to Geometry of Interaction, Course given at the Thematic School "Linear Logic, Ludics and Geometry of Interaction", August 29th 2012, Paraty, Brazil. pdf

Interaction Graphs: The Additive Construction, June 14th 2012, LOGOI Meeting, Marseillepdf

Graphs of Interaction: Additives, February 8th, 2012, LI2012, Marseille pdf

Graphs of Interaction : Multiplicatives, March 21st, 2010, GaLoP V, Paphos, Cyprus pdf

Graphes d'interaction, March 4th 2010, talk at the IMLpdf

#### Other Documents: PhD thesis

Logique dans le Facteur Hyperfini: Géométrie de l'Interaction et Complexité, PhD Thesis pdf

Slides of the defence (in french): pdf

Description in English (20 pages): pdf

Slides of a short presentation (5min) at the "Journées Nationales du GdR-IM" (in French): pdf

#### Other Documents: Course Notes

Some notes on Gelfand's theorem I wrote for a working group at the IML (in French) : pdf

Notes of a Course on Set Theory (in french): pdf

Notes on Graph C$^{*}$-algebras and Dynamical Systems (incomplete): pdf

#### Other Documents: Reports (Master)

I also make available the two reports I made during my Master.First Year (in French) : La ludique, supervised by Jean-Baptiste Joinet. pdf

Second Year (in English) : From Proof Nets to the hyperfinite factor, supervised by Claudia Faggian. (preliminary version) pdf