# Research

## Documents

#### Pre-Publications

Multiplicative linear logic from a resolution-based tile system, with Boris Eng, July 2022.

We present the stellar resolution, a "flexible" tile system based on Robinson's first-order resolution. After establishing formal definitions and basic properties of the stellar resolution, we show its Turing-completeness and to illustrate the model, we exhibit how it naturally represents computation with Horn clauses and automata as well as nondeterministic tiling constructions used in DNA computing. In the second and main part, by using the stellar resolution, we formalise and extend ideas of a new alternative to proof-net theory sketched by Girard in his transcendental syntax programme. In particular, we encode both cut-elimination and logical correctness for the multiplicative fragment of linear logic (MLL). We finally obtain completeness results for both MLL and MLL extended with the so-called MIX rule. By extending the ideas of Girard's geometry of interaction, this suggests a first step towards a new understanding of the interplay between logic and computation where linear logic is seen as a (constructed) way to format computation.

@unpublished{seiller-stellar,

Author = {Eng, Boris and Seiller, Thomas},

Title = {Multiplicative linear logic from a resolution-based tile system},

Note = {hal-03725336},

Year = {2022},

}

Author = {Eng, Boris and Seiller, Thomas},

Title = {Multiplicative linear logic from a resolution-based tile system},

Note = {hal-03725336},

Year = {2022},

}

A Novel Loop Fission Technique Inspired by Implicit Computational Complexity, with C. Aubert, T. Rubiano and N. Rusch, May 2022.

This work explores an unexpected application of Implicit Computational Complexity (ICC) to parallelize loops in imperative programs. Thanks to a lightweight dependency analysis, our algorithm allows splitting a loop into multiple loops that can be run in parallel, resulting in gains in terms of execution time similar to state-of-the-art automatic parallelization tools when both are applicable. Our graph-based algorithm is intuitive, language-agnostic, proven correct, and applicable to all types of loops, even if their loop iteration space is unknown statically or at compile time, if they are not in canonical form or if they contain loop-carried dependency. As contributions we deliver the computational technique, proof of its preservation of semantic correctness, and experimental results to quantify the expected performance gains. Our benchmarks also show that the technique could be seamlessly integrated into compiler passes or other automatic parallelization suites. We assert that this original and automatable loop transformation method was discovered thanks to the “orthogonal” approach offered by ICC.

@unpublished{seiller-pyalp,

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

Title = {A Novel Loop Fission Technique Inspired by Implicit Computational Complexity},

Year = {2022},

}

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

Title = {A Novel Loop Fission Technique Inspired by Implicit Computational Complexity},

Year = {2022},

}

Zeta functions and the (linear) logic of Markov processes, January 2021.

In a series of papers, Seiller introduced models of linear logic known as ”Interaction Graphs”. These models generalise Girard’s various geometry of interaction constructions, providing a unifying framework for those. In this work, we exhibit how these models can be understood mathematically through a cocycle property satisfied by zeta functions of dynamical systems. Focussing on probabilistic models, we then explain how the notion of graphings used in the models captures a natural class of Markov processes. We further extend previous constructions to provide a model of second-order linear logic as a type system over the set of all (discrete-time) sub-Markov processes.

@unpublished{seiller-MarkovZeta,

Author = {Seiller, Thomas},

Title = {Zeta functions and the (linear) logic of Markov processes},

Note = {\url{https://hal.archives-ouvertes.fr/hal-02458330}},

Year = {2021},

}

Author = {Seiller, Thomas},

Title = {Zeta functions and the (linear) logic of Markov processes},

Note = {\url{https://hal.archives-ouvertes.fr/hal-02458330}},

Year = {2021},

}

Lower bounds for algebraic machines, semantically, with L. Pellissier, January 2021.

This paper presents a new semantic method for proving lower bounds in computational complexity. We use it to prove that maxflow, a Ptime complete problem, is not computable in polylogarithmic time on parallel random access machines (prams) working with real numbers, showing that C ≠ Ptime, where C is the complexity class defined by such machines, and Ptime is the standard class of polynomial time computable problems (on, say, a Turing machine). On top of showing this new separation result, we show our method captures previous lower bounds results from the literature: Steele and Yao’s lower bounds for algebraic decision trees, Ben-Or’s lower bounds for algebraic computation trees, Cucker’s proof that NC_R is not equal to Ptime_R, and Mulmuley’s lower bounds for “prams without bit operations”.

@unpublished{seiller-PRAMsLB,

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

Title = {Lower bounds for algebraic machines, semantically},

Note = {\url{https://hal.archives-ouvertes.fr/hal-01921942}},

Year = {2021},

}

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

Title = {Lower bounds for algebraic machines, semantically},

Note = {\url{https://hal.archives-ouvertes.fr/hal-01921942}},

Year = {2021},

}

Agafonov’s Theorem for finite and infinite alphabets and probability distributions different from equidistribution, with Jakob G. Simonsen, November 2020.

An infinite sequence over a finite alphabet Σ of symbols is called normal iff the limiting frequency of every finite string w exists and equals |Σ|^{|w|}. A celebrated theorem by Agafonov states that a sequence α is normal iff every finite-state selector (i.e., a DFA accepting or rejecting prefixes of α) selects a normal sequence from α.

Let µ : Σ* → [0, 1] be a probability map (e.g. for all integer n, the sum of µ(w) when w ranges over words of length n is equal to 1). We say that an infinite sequence α is is µ-distributed if, for every finite string w, the limiting frequency of w in α exists and equals µ(w). Thus, α is normal if it is µ-distributed for the equidistributed probability map. Unlike normality, µ-distributedness is not preserved by finite-state selectors for all probability maps µ. This raises the question of how to characterize the probability maps µ for which µ-distributedness is preserved across finite-state selection, or equivalently, by selection by programs using constant space.

We prove the following result: for any finite or countably infinite alphabet Σ, every finite-state selector over Σ selects a µ-distributed sequence from every µ-distributed sequence α iff µ is induced by a Bernoulli distribution on Σ, that is a probability distribution on the alphabet extended to words by taking the product. The primary-and remarkable-consequence of our main result is a complete characterization of the set of probability maps, on finite and infinite alphabets, for which Agafonov-type results hold. The main positive takeaway is that (the appropriate generalization of) Agafonov's Theorem holds for Bernoulli distributions (rather than just equidistributions) on both finite and countably infinite alphabets.

As a further consequence, we obtain a result in the area of symbolic dynamical systems: the shift-invariant measures ν on Σ ω such that any finite-state selector preserves the property of genericity for ν, are exactly the positive Bernoulli measures.

Let µ : Σ* → [0, 1] be a probability map (e.g. for all integer n, the sum of µ(w) when w ranges over words of length n is equal to 1). We say that an infinite sequence α is is µ-distributed if, for every finite string w, the limiting frequency of w in α exists and equals µ(w). Thus, α is normal if it is µ-distributed for the equidistributed probability map. Unlike normality, µ-distributedness is not preserved by finite-state selectors for all probability maps µ. This raises the question of how to characterize the probability maps µ for which µ-distributedness is preserved across finite-state selection, or equivalently, by selection by programs using constant space.

We prove the following result: for any finite or countably infinite alphabet Σ, every finite-state selector over Σ selects a µ-distributed sequence from every µ-distributed sequence α iff µ is induced by a Bernoulli distribution on Σ, that is a probability distribution on the alphabet extended to words by taking the product. The primary-and remarkable-consequence of our main result is a complete characterization of the set of probability maps, on finite and infinite alphabets, for which Agafonov-type results hold. The main positive takeaway is that (the appropriate generalization of) Agafonov's Theorem holds for Bernoulli distributions (rather than just equidistributions) on both finite and countably infinite alphabets.

As a further consequence, we obtain a result in the area of symbolic dynamical systems: the shift-invariant measures ν on Σ ω such that any finite-state selector preserves the property of genericity for ν, are exactly the positive Bernoulli measures.

@unpublished{seiller-AgafonovIFF,

Author = {Seiller, Thomas and Simonsen, Jakob Grue},

Title = {Agafonov’s Theorem for finite and infinite alphabets and probability distributions different from equidistribution},

Note = {hal-02993635},

Year = {2020},

}

Author = {Seiller, Thomas and Simonsen, Jakob Grue},

Title = {Agafonov’s Theorem for finite and infinite alphabets and probability distributions different from equidistribution},

Note = {hal-02993635},

Year = {2020},

}

Agafonov’s Proof of Agafonov’s Theorem: A Modern Account and New Insights, with Jakob G. Simonsen, July 2020.

We give a modern account of Agafonov’s original proof of his eponymous theorem. The original proof was only reported in Russian in a journal not widely available, and the work most commonly cited in western literature is instead the English translation of a summary version containing no proofs, and the main proof relied heavily on material well-known in Russian mathematical circles of the day, which perhaps obscures the main thrust of argumentation for modern readers.

Our present account recasts Aganofov’s arguments using more basic building blocks than in the original proof, and contains some further embellishments to Agafonov’s original arguments, made in the interest of clarity. We posit that the modern account provides new insight to the underlying phenomena of the theorem.

We also provides some historical context to Agafonov’s work, including a short description of some of the ideas that led to Agafonov’s own proof, especially emphasizing the important work of Postnikova.

Our present account recasts Aganofov’s arguments using more basic building blocks than in the original proof, and contains some further embellishments to Agafonov’s original arguments, made in the interest of clarity. We posit that the modern account provides new insight to the underlying phenomena of the theorem.

We also provides some historical context to Agafonov’s work, including a short description of some of the ideas that led to Agafonov’s own proof, especially emphasizing the important work of Postnikova.

@unpublished{seiller-Agafonov,

Author = {Seiller, Thomas and Simonsen, Jakob Grue},

Title = {An Embellished Account of Agafonov’s Proof of Agafonov’s Theorem},

Note = {hal-02891463},

Year = {2020},

}

Author = {Seiller, Thomas and Simonsen, Jakob Grue},

Title = {An Embellished Account of Agafonov’s Proof of Agafonov’s Theorem},

Note = {hal-02891463},

Year = {2020},

}

Probabilistic complexity classes through semantics, January 2020.

In a recent paper, the author has shown how Interaction Graphs models for linear logic can be used to obtain implicit characterisations of non-deterministic complexity classes. In this paper, we show how this semantic approach to Implicit Complexity Theory (ICC) can be used to characterise deterministic and probabilistic models of computation. In doing so, we obtain correspondences between group actions and both deterministic and probabilistic hierarchies of complexity classes. As a particular case, we provide the first implicit characterisations of the classes PL (unbounded error probabilistic logarithmic space) and PP (unbounded error probabilistic polynomial time).

@unpublished{seiller-Prob-ICC,

Author = {Seiller, Thomas},

Title = {Probabilistic complexity classes through semantics},

Note = {Submitted},

Year = {2020},

}

Author = {Seiller, Thomas},

Title = {Probabilistic complexity classes through semantics},

Note = {Submitted},

Year = {2020},

}

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

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

}

#### Publications: Journals

From abstraction and indiscernibility to classification and types: revisiting Hermann Weyl’s theory of ideal elements, with J. B. Joinet, 科学哲学 (Kagaku tetsugaku) 53, 2021.

@article{seiller-Weyl,

Author = {Joinet, Jean-Baptiste and Seiller, Thomas},

Title = {From abstraction and indiscernibility to classification and types: revisiting Hermann Weyl’s theory of ideal elements},

Journal = {Kagaku tetsugaku},

Volume = {53},

Number = {2},

Pages = {65-93},

Year = {2021},

DOI = {10.4216/jpssj.53.2_65},

}

Author = {Joinet, Jean-Baptiste and Seiller, Thomas},

Title = {From abstraction and indiscernibility to classification and types: revisiting Hermann Weyl’s theory of ideal elements},

Journal = {Kagaku tetsugaku},

Volume = {53},

Number = {2},

Pages = {65-93},

Year = {2021},

DOI = {10.4216/jpssj.53.2_65},

}

Interaction Graphs: Exponentials. Logical Methods in Computer Science 15, 2019.

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 = {2019},

Volume = {15},

Number = {3},

DOI = {10.23638/LMCS-15(3:25)2019},

}

Author = {Seiller, Thomas},

Title = {Interaction Graphs: Exponentials},

Journal = {Logical Methods in Computer Science},

Year = {2019},

Volume = {15},

Number = {3},

DOI = {10.23638/LMCS-15(3:25)2019},

}

Coherent Interaction Graphs, with L.T.D. Nguyễn, Electronic Proceedings in Theoretical Computer Science (EPTCS), Post-Proceedings of TLLA-Linearity 2018.

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

Journal = {Electronic Proceedings in Theoretical Computer Science},

Year = {2019},

VOLUME = {292},

PAGES = {104-117},

DOI = {10.4204/EPTCS.292.6},

}

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

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

Journal = {Electronic Proceedings in Theoretical Computer Science},

Year = {2019},

VOLUME = {292},

PAGES = {104-117},

DOI = {10.4204/EPTCS.292.6},

}

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

mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity, with C. Aubert, T. Rubiano and N. Rusch, FSCD 2022. Related software: https://pypi.org/project/pymwp.

Implicit Computational Complexity (ICC) drives better understanding of complexity classes, but it also guides the development of resources-aware languages and static source code analyzers.
Among the methods developed, the mwp-flow analysis certifies polynomial bounds on the size of the values manipulated by an imperative program.
This result is obtained by bounding the transitions between states instead of focusing on states in isolation, as most static analyzers do, and is not concerned with termination or tight bounds on values.
Those differences, along with its built-in compositionality, make the mwp-flow analysis a good target for determining how ICC-inspired techniques diverge compared with more traditional static analysis methods.
This paper's contributions are three-fold: we fine-tune the internal machinery of the original analysis to make it tractable in practice; we extend the analysis to function calls and leverage its machinery to compute the result of the analysis efficiently; and we implement the resulting analysis as a lightweight tool to automatically perform data-size analysis of C programs.

This documented effort prepares and enables the development of certified complexity analysis, by transforming a costly analysis into a tractable program, that furthermore decorrelates the problem of deciding if a bound exist with the problem of computing it.

This documented effort prepares and enables the development of certified complexity analysis, by transforming a costly analysis into a tractable program, that furthermore decorrelates the problem of deciding if a bound exist with the problem of computing it.

@unpublished{seiller-pymwp-tool,

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

Title = {mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity},

Booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},

Year = {2022},

doi = {10.4230/LIPIcs.FSCD.2022.26},<\span>

}

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

Title = {mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity},

Booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},

Year = {2022},

doi = {10.4230/LIPIcs.FSCD.2022.26},<\span>

}

A cartesian bicategory of polynomial functors in homotopy type theory, with E. Finster, S. Mimram and M. Lucas, MFPS 2021.

Polynomial functors are a categorical generalization of the usual notion of polynomial, which has found many applications in higher categories and type theory: those are generated by polynomials consisting a set of monomials built from sets of variables. They can be organized into a cartesian bicategory, which unfortunately fails to be closed for essentially two reasons, which we address here by suitably modifying the model. Firstly, a naive closure is too large to be well-defined, which can be overcome by restricting to polynomials which are finitary. Secondly, the resulting putative closure fails to properly take the 2-categorical structure in account. We advocate here that this can be addressed by considering polynomials in groupoids, instead of sets. For those, the constructions involved into composition have to be performed up to homotopy, which is conveniently handled in the setting of homotopy type theory: we use it here to formally perform the constructions required to build our cartesian bicategory, in Agda. Notably, this requires us introducing an axiomatization in a small universe of the type of finite types, as an appropriate higher inductive type of natural numbers and bijections.

@inproceedings{seiller-MFPS,

Author = {Finster, Éric and Mimram, Samuel and Rubiano, Thomas and Seiller, Thomas},

Title = {A cartesian bicategory of polynomial functors in homotopy type theory},

Booktitle = {37th Conference on Mathematical Foundations of Programming Semantics (MFPS 2021)},

Year = {2021},

DOI = {10.4204/EPTCS.351.5},

}

Author = {Finster, Éric and Mimram, Samuel and Rubiano, Thomas and Seiller, Thomas},

Title = {A cartesian bicategory of polynomial functors in homotopy type theory},

Booktitle = {37th Conference on Mathematical Foundations of Programming Semantics (MFPS 2021)},

Year = {2021},

DOI = {10.4204/EPTCS.351.5},

}

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

A gentle introduction to Girard's Transcendental Syntax, with B. Eng, TLLA 2021.

We present a gentle introduction to the technical content of Girard's Transcendental Syntax suggesting a new framework for the proof theory of linear logic and an alternative understanding of proof-nets. In this framework, we investigate the emergence of logic from a model of computation related to tiling models and logic programs.

@inproceedings{seiller-gentleintro,

Author = {Eng, Boris and Seiller, Thomas},

Title = {A gentle introduction to Girard's Transcendental Syntax},

Year = {2021},

Booktitle = {{5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021)}},

URL = {https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271496},

HAL_ID = {lirmm-03271496},

}

Author = {Eng, Boris and Seiller, Thomas},

Title = {A gentle introduction to Girard's Transcendental Syntax},

Year = {2021},

Booktitle = {{5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021)}},

URL = {https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271496},

HAL_ID = {lirmm-03271496},

}

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 Python implementation of MWP flow analysis, https://pypi.org/project/pymwp, Implementation in Python of MWP flow analysis to analyse data complexity of C programs. GitHub page: https://github.com/seiller/pymwp.

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

}

Les limites de la parallélisation du calcul. Gazette de la Recherche de l'Institut Galilée, Université Paris 13.

pdf

A one-page popularised account (in French) of the PRAMs lower bounds result in collaboration with Luc Pellissier.

@inproceedings{seiller-Gazette,

Author = {Seiller, Thomas},

Title = {Les limites de la parallélisation du calcul},

Booktitle = {Gazette de l'Institut Galilée},

Editor = {Uniiversité Paris Nord},

Pages = {6},

Year = {2019},

}

Author = {Seiller, Thomas},

Title = {Les limites de la parallélisation du calcul},

Booktitle = {Gazette de l'Institut Galilée},

Editor = {Uniiversité Paris Nord},

Pages = {6},

Year = {2019},

}

#### Pre-Publications: 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},

}

Normal Sequences and Selection Rules: Beyond Agafonov's Theorem, with J. G . Simonsen, in preparation.

@unpublished{seiller-IGPure,

Author = {Seiller, Thomas and Simonsen, Jakob Grue},

Title = {Normal Sequences and Selection Rules: Beyond Agafonov's Theorem},

Note = {in preparation},

}

Author = {Seiller, Thomas and Simonsen, Jakob Grue},

Title = {Normal Sequences and Selection Rules: Beyond Agafonov's Theorem},

Note = {in preparation},

}

#### Other Documents: Workshops, Technical Reports

Multiplicative Linear Logic from Logic Programs and Tilings, with Boris Eng, January 2021.

We present a non-deterministic model of computation related to Robinson’s first-order resolution. This model formalises and extends ideas sketched by Girard in his Transcendental Syntax programme. After establishing formal definitions and basic properties, we show its Turing-completeness by exhibiting how it naturally models logic programs as well as non-deterministic tiling constructions such as those defining the abstract tile assembly model, recently used in DNA computing. In a second part, we explain how this model of computation yields, using realisability techniques, a dynamic semantics of proofs in the multiplicative fragment of linear logic (MLL), for which we obtain full-completeness results for both MLL and MLL extended with the so-called MIX rule.

@unpublished{seiller-stellar,

Author = {Eng, Boris and Seiller, Thomas},

Title = {Multiplicative Linear Logic from Logic Programs and Tilings},

Note = {hal-02895111},

Year = {2021},

}

Author = {Eng, Boris and Seiller, Thomas},

Title = {Multiplicative Linear Logic from Logic Programs and Tilings},

Note = {hal-02895111},

Year = {2021},

}

An extended and more practical mwp flow analysis, with C. Aubert, T. Rubiano and N. Rusch, June 2021. Research paper presenting the theory behind the https://pypi.org/project/pymwp Software.

We improve and refine a method for certifying that the values’ sizes computed by an imperative program will be bounded by polynomials in the program’s inputs’ sizes. Our work “tames” the non-determinism of the original analysis, and offers an innovative way of completing the analysis when a non-polynomial growth is found. We furthermore enrich the analyzed language by adding function definitions and calls, allowing to compose the analysis of different libraries and offering generally more modularity. The implementation of our improved method, discussed in a tool paper, also required to reason about the efficiency of some of the needed operations on the matrices produced by the analysis. It is our hope that this work will enable and facilitate static analysis of source code to guarantee its correctness with respect to resource usages.

@unpublished{seiller-pymwp,

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

Title = {An extended and more practical mwp flow analysis},

Note = {},

Year = {2021},

}

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

Title = {An extended and more practical mwp flow analysis},

Note = {},

Year = {2021},

}

An implementation of flow calculus for complexity analysis (tool paper), with C. Aubert, T. Rubiano and N. Rusch, June 2021. Tool paper presenting the https://pypi.org/project/pymwp Software.

We present a tool to automatically perform the datasize analysis of imperative programs written in C. This tool, called pymwp, is inspired by a classical work on complexity analysis, and allows to certify that the size of the values computed by a program will be bounded by a polynomial in the program’s inputs. Strategies to provide meaningful feedback on non-polynomial programs and to “tame” the non-determinism of the original analysis were implemented following recent progresses, but required particular care to accommodate the growing complexity of the analysis.

The Python source code is intensively documented, and our numerous example files encompass the original examples as well as multiple test cases. A pip package should make it easy to install pymwp on any plat-form, but an on-line demo is also available for convenience.

The Python source code is intensively documented, and our numerous example files encompass the original examples as well as multiple test cases. A pip package should make it easy to install pymwp on any plat-form, but an on-line demo is also available for convenience.

@unpublished{seiller-pymwp-tool,

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

Title = {An implementation of flow calculus for complexity analysis (tool paper)},

Note = {},

Year = {2021},

}

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

Title = {An implementation of flow calculus for complexity analysis (tool paper)},

Note = {},

Year = {2021},

}

A cartesian bicategory of polynomial functors in homotopy type theory, with E. Finster, M. Lucas and S. Mimram, May 2021.

Polynomial functors are a categorical generalization of the usual notion of polynomial, which has found many applications in higher categories and type theory: those are generated by polynomials consisting a set of monomials built from sets of variables. They can be organized into a cartesian bicategory, which unfortunately fails to be closed for essentially two reasons, which we address here by suitably modifying the model. Firstly, a naive closure is too large to be well-defined, which can be overcome by restricting polynomials which are finitary. Secondly, the resulting putative closure fails to properly take the 2-categorical structure in account. We advocate here that this can be addressed by considering polynomials in groupoids, instead of sets. For those, the constructions involved into composition have to be performed up to homotopy, which is conveniently handled in the setting of homotopy type theory, that we use here, in Agda, to formally perform the constructions required to build our cartesian bicategory. Notably, this requires us introducing an axiomatization in a small universe of the type of finite types, as an appropriate higher inductive type of natural numbers and bijections.

@unpublished{seiller-CartBiHoTT,

Author = {Finster, Eric and Lucas, Maxime and Mimram, Samuel and Seiller, Thomas},

Title = {A cartesian bicategory of polynomial functors in homotopy type theory},

Note = {},

Year = {2021},

}

Author = {Finster, Eric and Lucas, Maxime and Mimram, Samuel and Seiller, Thomas},

Title = {A cartesian bicategory of polynomial functors in homotopy type theory},

Note = {},

Year = {2021},

}

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: Unpublished work

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

}

A correctness criterion for trees, 2009.

This is an excerpt from a draft dates 2009, in which I describe a correctness criterion for trees (and prove it does the job). The initial project (which was abandoned) was to find an analogue of Girard's "longtrips" correctness criterion for MALL proof nets. Since then, I found myself sharing this document since it somehow explains the equivalence between Girard's criterion and the one provided by Danos and Regnier. But more interestingly (equiv. unexpectedly), it turns out that this theorem, when reformulated in the words of graph theory, implies that a connected graph is a tree iff all its cellular embeddings on surfaces have a single face.

@unpublished{seiller-CCTres,

Author = {Seiller, Thomas},

Title = {A correctness criterion for trees},

Note = {},

Year = {2009},

}

Author = {Seiller, Thomas},

Title = {A correctness criterion for trees},

Note = {},

Year = {2009},

}

#### Other Documents: Slides

DICE-FOPARA 2019, April 6-7th 2019, Prague, Czech Republic. pdf

Journées inaugurales "Logique, Homotopie, Catégories, October 17-18th 2018, Marseille, France. pdf

Conference on Mathematical Logic, August 10-11th 2018, Satellite event of the ICM 2018, Niterói, Brazil. Slides.

Cologne-Twente Workshop on Graphs and Combinatorial Optimisation, June 18-20th 2018, Paris, France. pdf

Workshop on Realisability, June 12-13th 2018, CIRM, Marseille, France. pdf

Thirty Years of Linear Logic conference, October 25th 2017, Rome, Italy. 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