Research

Documents

Habilitation thesis

Mathematical Informatics, April 2024. Slides from the defence: pdf.
pdf Abstract Bibtex
TEL: tel-04616661
What is a model of computation? What is a program, an algorithm? While theoretical computer science has been founded on computability theory, the latter does not answer these questions. Indeed, it is a mathematical theory of computable functions, and does not account for computation itself. A symptomatic consequence is the notion of Turing-completeness. This standard (sole?) equivalence between models of computation is purely extensional: it does only care about what is computed and not how, blind to complexity aspects and the question of algorithmic completeness. More importantly, the theory of computation is continuously growing further from how actual machines compute.
I present a proposal for alternative foundations more faithful to computer science practice and interests. This mathematisation of computer science is grounded within the theory of dynamical systems, focussing on *how* computation is performed rather than only on *what* is computed. I will argue that it generalises computability theory while still allowing to recover standard results.
Moreover, this dynamical point of view can be used to:
  • propose a formal definition of the notion of algorithm
  • define static analysis methods which can be implemented in usable tools
  • provide a uniform account of several lower bounds from algebraic complexity and strengthen them
  • define families of linear realisability models (realisability models for linear logic)
  • lead to a semantic approach of implicit computational complexity
@thesis{seiller-HdR,
Author = {Seiller, Thomas},
Title = {Mathematical Informatics},
Year = {2024},
School = {Sorbonne Paris Nord University},
Note = {Habilitation thesis},
Url = {https://theses.hal.science/tel-04616661},
}

Pre-Publications

Kolmogorov time hierarchy and novelty games, with U. Léchine, April 2024.
pdf Abstract Bibtex
HAL: hal-04539439
In this paper we improve on the state-of-the-art time hierarchy for time-bounded Kolmogorov complexity. More precisely, we prove that there are infinitely many integers n such that there are strings of size n which are the output of programs of size f = o(log n) running in o(2f T) steps but are not the output of any program of size f running in T steps. The previous gap was exponential in 2f. This result is established by studying a new problem in combinatorics: a list E of pk numbers in [1; N] is shared evenly between p players, who each get to output an answer depending on their share of E. The players must establish a communication-free strategy ensuring that one of them outputs a number not belonging to E.
@unpublished{seiller-TBK,
Author = {Léchine, Ulysse and Seiller, Thomas},
Title = {Kolmogorov time hierarchy and novelty games},
Note = {Submitted},
Year = {2024},
}
Simplifying normal functors: an old and a new model of the λ-calculus, with M. Rogers and W. Troiani, January 2024.
pdf Abstract Bibtex
HAL: hal-04500078
The introduction of Linear Logic by Jean-Yves Girard takes its origins in the so-called normal functors model of lambda-calculus in which untyped λ-terms are interpreted as ‘normal functors’ between presheaf categories. As a result, we produce a new model in ‘normal functions’ between sets of (possibly infinite) multisets, gaining new insights on Girard’s original construction. We then extend this to an explicit model of intuitionistic Linear Logic, contrasting the result with the weighted relational model.
@unpublished{seiller-simpleNF,
Author = {Rogers, Morgan and Seiller, Thomas and Troiani, William},
Title = {Simplifying normal functors: an old and a new model of the λ-calculus},
Note = {Submitted},
Year = {2024},
}
Implicit complexity through linear realisability: polynomial time and probabilistic classes, January 2023.
pdf Abstract Bibtex
HAL: hal-02458358
Based on work on realisability models for linear logic, the author recently proposed a new approach of implicit computational complexity. He showed how to characterise in this way a hierarchy of sub-linear space non-deterministic complexity classes by means of group actions. These classes, defined by means of two-way non-deterministic automata, range from regular languages to NLogspace (non-deterministic logarithmic space).
In the present paper, we extend those results in two directions. First, we show how the same techniques can be used to characterise the sub-linear space complexity classes defined by both deterministic and probabilistic two-way multi-head automata. We thus obtain characterisations of deterministic complexity classes between regular languages and Logspace, as well as a hierarchy of probabilistic classes between stochastic languages and PLogspace (unbounded error probabilistic logarithmic space). Second, we exhibit a monoid action capturing polynomial time computation based on pushdown machines, characterising both Ptime and PPtime (unbounded error probabilistic polynomial time).
@unpublished{seiller-Prob-ICC,
Author = {Seiller, Thomas},
Title = {Implicit complexity through linear realisability: polynomial time and probabilistic classes},
Note = {Submitted},
Year = {2023},
}
Multiplicative Linear Logic from Logic Programs and Tilings, with Boris Eng, 2021.
pdf Abstract Bibtex
HAL: hal-02895111
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},
}
Agafonov’s Proof of Agafonov’s Theorem: A Modern Account and New Insights, with Jakob G. Simonsen, July 2020.
pdf Abstract Bibtex
HAL: hal-02891463
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.
@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},
}
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.
pdf Abstract Bibtex
HAL: hal-01979009v1
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},
}

Publications: Under revision

Agafonov’s Theorem for finite and infinite alphabets and probability distributions different from equidistribution, with Jakob G. Simonsen, November 2022. Under revision for publication in Ergodic Theory and Dynamical Systems.
pdf Abstract Bibtex
HAL: hal-02993635
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.
@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 = {2022},
}

Publications: Journals

Unifying lower bounds for algebraic machines, semantically, with L. Pellissier and U. Léchine. Information and Computation 301, 2024.
pdf Abstract Bibtex
doi:10.1016/j.ic.2024.105232 HAL: hal-01921942
This paper presents a new abstract method for proving lower bounds in computational complexity. Based on the notion of topological and measurable entropy for dynamical systems, it is shown to generalise three previous lower bounds results from the literature in algebraic 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. This improves, albeit slightly, on a result of Mulmuley since the class of machines considered extends the class “prams without bit operations”, making more precise the relationship between Mulmuley’s result and similar lower bounds on real prams.
More importantly, we show our method captures previous lower bounds results from the literature, thus providing a unifying framework for "topological" proofs of lower bounds: Steele and Yao’s lower bounds for algebraic decision trees, Ben-Or’s lower bounds for algebraic computation trees, Cucker’s proof that NC is not equal to Ptime in the real case, and Mulmuley’s lower bounds for “prams without bit operations”.
@unpublished{seiller-PRAMsLB,
Author = {Seiller, Thomas and Pellissier, Luc and Léchine, Ulysse},
Title = {Unifying lower bounds for algebraic machines, semantically},
Journal = {Information and Computation},
Volume = {301},
Year = {2024},
Doi = {10.1016/j.ic.2024.105232},
}
Zeta functions and the (linear) logic of Markov processes, Logical Methods in Computer Science 20(3), 2024.
pdf Abstract Bibtex
doi:10.46298/lmcs-20(3:18)2024 HAL: hal-02458330
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.
@article{seiller-MarkovZeta,
Author = {Seiller, Thomas},
Title = {Zeta functions and the (linear) logic of Markov processes},
Journal = {Logical Methods in Computer Science},
Year = {2024},
Volume = {{Volume 20, Issue 3}},
Doi = {10.46298/lmcs-20(3:18)2024},
}
From abstraction and indiscernibility to classification and types: revisiting Hermann Weyl’s theory of ideal elements, with J. B. Joinet, 科学哲学 (Kagaku tetsugaku) 53, 2021.
pdf Abstract Bibtex
doi:10.4216/jpssj.53.2_65

@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},
}
Interaction Graphs: Exponentials. Logical Methods in Computer Science 15, 2019.
pdf Abstract Bibtex
doi:10.23638/LMCS-15(3:25)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},
}
Coherent Interaction Graphs, with L.T.D. Nguyễn, Electronic Proceedings in Theoretical Computer Science (EPTCS), Post-Proceedings of TLLA-Linearity 2018.
pdf Abstract Bibtex
doi:10.4204/EPTCS.292.6
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},
}
Interaction Graphs: Nondeterministic Automata, ACM Transactions in Computational Logic 19(3), 2018.
pdf Abstract Bibtex
doi:10.1145/3226594
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},
}
A Correspondence between Maximal Abelian Sub-Algebras and Linear Logic Fragments, Mathematical Structures in Computer Science 28(1), 2018
pdf Abstract Bibtex
doi:10.1017/S0960129516000062
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},
}
An Intentionally Fully-Abstract Sheaf Model For π (Extended Version), with Clovis Eberhart and Tom Hirschowitz. Logical Methods in Computer Science 13(4), 2017.
pdf Abstract Bibtex
doi:10.23638/LMCS-13(4:9)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},
}
Interaction Graphs: Graphings, Annals of Pure and Applied Logic 168 (2017), pp. 278–320.
pdf Abstract Bibtex
doi:10.1016/j.apal.2016.10.007
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},
}
Logarithmic Space and Permutations, with C. Aubert. Information and Computation 248 (2016), pp. 2–21.
pdf Abstract Bibtex
doi:10.1016/j.ic.2014.01.018
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},
}
Characterizing co-NL by a group action, with C. Aubert. Mathematical Structures in Computer Science 26 (2016), pp. 606—638.
pdf Abstract Bibtex
doi:10.1017/S0960129514000267
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},
}
Interaction Graphs: Additives, Annals of Pure and Applied Logic 167 (2016), pp. 95-154.
pdf Abstract Bibtex
doi:10.1016/j.apal.2015.10.001
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},
}
Interaction Graphs: Multiplicatives, Annals of Pure and Applied Logic 163 (2012), pp. 1808-1837.
pdf Abstract Bibtex
doi:10.1016/j.apal.2012.04.005
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},
}

Publications: Conferences

Linear realisability on untyped nets, with A. Ragot and L. Tortora de Falco, CSL 2025.
pdf Abstract Bibtex
HAL: hal-04432854
We present a new realisability model based on orthogonality for Linear Logic in the context of nets-untyped proof structures with generalized axiom. We show that it adequately models second order multiplicative linear logic. As usual, not all realizers are representations of a proof, but we identify specific types (sets of nets closed under bi-othogonality) that capture exactly the proofs of a given sequent thus proving a completeness theorem. Furthermore these types are orthogonal's of finite sets; this ensures the existence of a correctnesss criterion that runs in finite time.
@inproceedings{seiller-RealNet,
Author = {Ragot, Adrien and Seiller, Thomas and Tortora de Falco, Lorenzo},
Title = {Linear realisability over untyped nets},
Booktitle = {CSL 2025},
Year = {2025},
}
Agafonov's theorem for probabilistic selectors, with U. Léchine and J. G. Simonsen, MFCS 2024.
pdf Abstract Bibtex
HAL: hal-03269121v4
A normal sequence over {0,1} is an infinite sequence for which every word of length k appears with frequency 2^{-k}. Agafonov's eponymous theorem states that selection by a finite state selector preserves normality, i.e. if α is a normal sequence and S is a finite state selector, then the subsequence S(α) is either finite or a normal sequence.
In this work, we address the following question: does this result hold when considering probabilistic selectors? We provide a partial positive answer, in the case the probabilities involved are rational. More formally, we prove that given a normal sequence α and a rational probabilistic selector S, the selected subsequence S(α) will be a normal sequence with probability 1.
@inproceedings{seiller-ProbAgafonov,
Author = {Léchine, Ulysse and Seiller, Thomas and Simonsen, Jakob Grue},
Title = {Agafonov's theorem for probabilistic selectors},
Booktitle = {49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
doi = {10.4230/LIPIcs.MFCS.2024.67},
Year = {2024},
}
pymwp: A Static Analyzer Determining Polynomial Growth Bounds, with C. Aubert, T. Rubiano and N. Rusch, ATVA 2023.
pdf Abstract Bibtex
HAL: hal-03269121v4
We present pymwp, a static analyzer that automatically computes, if they exist, polynomial bounds relating input and output sizes. In case of exponential growth, our tool detects precisely which dependencies between variables induced it. Based on the sound mwp-flow calculus, the analysis captures bounds on large classes of programs by being non-deterministic and not requiring termination. For this reason, implementing this calculus required solving several non-trivial implementation problems, to handle its complexity and non-determinism, but also to provide meaningful feedback to the programmer. The duality of the analysis result and compositionality of the calculus make our approach original in the landscape of complexity analyzers. We conclude by demonstrating experimentally how pymwp is a practical and performant static analyzer to automatically evaluate variable growth bounds of C programs.
@inproceedings{seiller-atva23,
Author = {Aubert, Clément and Rubiano, Thomas and Rusch, Neea and Seiller, Thomas},
Title = {pymwp: A Static Analyzer Determining Polynomial Growth Bounds},
Booktitle = {21st International Symposium on Automated Technology for Verification and Analysis (ATVA 2023)},
Year = {2023},
doi = {10.1007/978-3-031-45332-8_14},
}
Distributing and Parallelizing Non-canonical Loops, with C. Aubert, T. Rubiano and N. Rusch, VMCAI 2023.
pdf Abstract Bibtex
doi:10.1007/978-3-031-24950-1_1
This work leverages an original dependency analysis to parallelize loops regardless of their form in imperative programs. Our algorithm distributes a loop into multiple parallelizable loops, resulting in gains in execution time comparable to state-of-the-art automatic source-to-source code transformers when both are applicable. Our graph-based algorithm is intuitive, language-agnostic, proven correct, and applicable to all types of loops. Importantly, it can be applied even if the loop iteration space is unknown statically or at compile time, or more generally if the loop is not in canonical form or contains 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. We also show that many comparable tools cannot distribute the loops we optimize, and that our technique can be seamlessly integrated into compiler passes or other automatic parallelization suites.
@inproceedings{seiller-vmcai,
Author = {Aubert, Clément and Rubiano, Thomas and Rusch, Neea and Seiller, Thomas},
Title = {Distributing and Parallelizing Non-canonical Loops},
Booktitle = {24th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2023)},
Year = {2023},
doi = {10.1007/978-3-031-24950-1_1},
}
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.
pdf Abstract Bibtex
doi:10.4230/LIPIcs.FSCD.2022.26
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.
@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},
}
A cartesian bicategory of polynomial functors in homotopy type theory, with E. Finster, S. Mimram and M. Lucas, MFPS 2021.
pdf Abstract Bibtex
doi:10.4204/EPTCS.351.5
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},
}
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.
pdf Abstract Bibtex
doi:10.1007/978-3-319-68167-2_7
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.
@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},
}
Interaction Graphs: Full Linear Logic, LICS 2016.
pdf Abstract Bibtex
doi:10.1145/2933575.2934568
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},
}
Unary Resolution: Characterizing Ptime, with Marc Bagnol and Clément Aubert, FOSSACS 2016.
pdf
Abstract Bibtex
doi:10.1007/978-3-662-49630-5_22
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},
}
An intensionally fully-abstract sheaf model for π, with Clovis Eberhart and Tom Hirschowitz. CALCO 2015. Best paper award.
pdf Abstract Bibtex
doi:10.4230/LIPIcs.CALCO.2015.86
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},
}
Logic Programming and Logarithmic Space, with C. Aubert, M. Bagnol and P. Pistone. APLAS 2014.
pdf Abstract Bibtex
doi:10.1007/978-3-319-12736-1_3
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},
}

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).
pdf Abstract Bibtex
doi:10.1007/978-3-319-20762-9_9
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},
}
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
Abstract Bibtex
doi:10.1007/978-3-319-26506-3_5
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},
}

Publications: Workshops

A gentle introduction to Girard's Transcendental Syntax, with B. Eng, TLLA 2021.
pdf Abstract Bibtex
HAL: lirmm-03271496v1
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},
}
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.
pdf Abstract Bibtex
doi:10.4204/EPTCS.248.9
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.
@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},
}

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: Encyclopedia entries

Algorithme, with Alberto Naibo. Encyclopædia Universalis, 2024.
Online version Bibtex
@inbook{seiller-algorithme,
Author = {Naibo, Alberto and Seiller, Thomas},
Title = {Algorithme},
Booktitle = {Encyclopædia Uversalis},
Year = {2024},
}

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 Abstract Bibtex
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},
}
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.
pdf Abstract Bibtex
doi:10.15496/publikation-18676
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},
}
Les limites de la parallélisation du calcul. Gazette de la Recherche de l'Institut Galilée, Université Paris 13.
pdf Abstract Bibtex
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},
}

Pre-Publications: In preparation

Logical Constants from a Computational Point of View, with Alberto Naibo and Mattia Petrolo, in preparation.
pdf Abstract Bibtex
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},
}
Linear realisability over Turing machines, in preparation.
pdf Abstract Bibtex
@unpublished{seiller-IGTM,
Author = {Seiller, Thomas},
Title = {Linear realisability over Turing machines},
Note = {in preparation},
}
Normal Sequences and Selection Rules: Beyond Agafonov's Theorem, with J. G . Simonsen, in preparation.
pdf Abstract Bibtex
@unpublished{seiller-BeyondAgafonov,
Author = {Seiller, Thomas and Simonsen, Jakob Grue},
Title = {Normal Sequences and Selection Rules: Beyond Agafonov's Theorem},
Note = {in preparation},
}
Linear realisability and cobordisms, with V. Maestracci, in preparation.
pdf Abstract Bibtex
@unpublished{seiller-Cobord,
Author = {Maestracci, Valentin and Seiller, Thomas},
Title = {Linear realisability and cobordisms},
Note = {in preparation},
}
Decategorifying normal functors, with M. Rogers and W. Troiani, in preparation.
pdf Abstract Bibtex
@unpublished{seiller-Decategorify,
Author = {Rogers, Morgan and Seiller, Thomas and Troiani, William},
Title = {Decategorifying normal functors},
Note = {in preparation},
}

Other Documents: Workshops, Technical Reports

Linear Realizability and Cobordisms, with V. Maestracci, TLLA 2023.
pdf Abstract Bibtex
@inproceedings{seiller-tlla2023-cobord,
Author = {Maestracci, Valentin and Seiller, Thomas},
Title = {Linear Realizability and Cobordisms},
Year = {2023},
}
Normal functors[ions], [the irrelevence of] power series, and [a new model of] 𝜆-calculus, with M. Rogers and W. Troiani, TLLA 2023.
pdf Abstract Bibtex
@inproceedings{seiller-tlla2023-normal,
Author = {Rogers, Morgan and Seiller, Thomas and Troiani, William},
Title = {Normal functors[ions], [the irrelevence of] power series, and [a new model of] 𝜆-calculus},
Year = {2023},
}
Linear realisability over nets and second order quantification, with A. Ragot and L. Tortora de Falco, TLLA 2023.
pdf Abstract Bibtex
HAL: hal-04131640
We extend the use of realizability techniques for Linear Logic to an untyped generalisation of proof nets. We obtain the results of soundness (e.g. adequacy) for second-order multiplicative linear logic and completeness for the quantifier-free fragment. Moreover we provide, to our knowledge, the first proper proof of the folklore result which states that ’tests of 𝐴 are proofs of its negation’.
@inproceedings{seiller-tlla2023-netreal,
Author = {Ragot, Adrien and Seiller, Thomas and Tortora de Falco, Lorenzo},
Title = {Linear realisability over nets and second order quantification},
Year = {2023},
}
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.
pdf Abstract Bibtex
HAL: hal-03269096
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},
}
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.
pdf Abstract Bibtex
HAL: hal-03269121
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.
@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},
}
A cartesian bicategory of polynomial functors in homotopy type theory, with E. Finster, M. Lucas and S. Mimram, May 2021.
pdf Abstract Bibtex
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},
}
A semantic conjecture on second-order MLL and its complexity consequences (work in progress), Abstract for Linearity-TLLA 2018.
pdf Abstract Bibtex
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},
}
Coherent Interaction Graphs: A Non-Deterministic Geometry of Interaction for MLL, Abstract for Linearity-TLLA 2018.
pdf Abstract Bibtex
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},
}
Entropy and Complexity Lower Bounds, Abstract for Linearity-TLLA 2018.
pdf Abstract Bibtex
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.
@unpublished{seiller-SECLBlin,
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 Abstract Bibtex
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.
@unpublished{seiller-SECLBabs,
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 Abstract Bibtex
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.
@unpublished{seiller-SECLB,
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 Abstract Bibtex
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},
}
Measurable Preorders and Complexity, Abstract for TACL 2015.
pdf Abstract Bibtex
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},
}
Memoization for Unary Logic Programming: Characterizing Ptime, Research report. Joint work with Marc Bagnol and Clément Aubert, January 2015.
pdf Abstract Bibtex
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},
}
Interaction Graphs and Complexity, Abstract.
pdf Abstract Bibtex
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},
}
Logarithmic Space and Permutations, Abstract for DICE 2013.
pdf Abstract Bibtex
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},
}

Other Documents: Unpublished work

From Dynamic to Static Semantics, Quantitatively.
pdf Abstract Bibtex
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},
}
Towards a Complexity-through-Realizability Theory.
pdf Abstract Bibtex
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},
}
A correctness criterion for trees, 2009.
pdf Abstract Bibtex
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},
}

Other Documents: Slides

TLLA 2024, July 8th 2024, Tallinn, Estonia. pdf
Structure meets Power 2024, July 7th 2024, Tallinn, Estonia. pdf
Proofs and Algorithms seminar, LIX, May 15th 2024, Palaiseau, France. pdf
Okada Lab seminar, Keio university, May 28th 2024, Tokyo, Japan. pdf
HaPoC 2023, October 18th-20th 2023, Warsaw, Poland. pdf
FSCD 2022, August 4th 2023, Haifa, Israel. pdf
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