12 citations · 21 across the 8 of their papers we have counts for
7 papers · 1 filter
An extended and more practical mwp flow analysis
Clément Aubert, Thomas Rubiano, Neea Rusch +1
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 ''tam…
Stellar Resolution: Multiplicatives
Boris Eng, Thomas Seiller
We present a new asynchronous model of computation named Stellar Resolution based on first-order unification. This model of computation is obtained as a formalisation of Girard's t…
Coherent Interaction Graphs
Lê Thành Dũng Nguyen, Thomas Seiller
We introduce the notion of coherent graphs, and show how those can be used to define dynamic semantics for Multiplicative Linear Logic (MLL) extended with non-determinism. Thanks t…
Around finite second-order coherence spaces
Lê Thành Dũng Nguyên
Many applications of denotational semantics, such as higher-order model checking or the complexity of normalization, rely on finite semantics for monomorphic type systems. We exhib…
From Dynamic to Static Semantics, Quantitatively
Thomas Seiller
We exhibit a new relationship between dynamic and static semantics. We define the categorical outlay needed to define Interaction Graphs models, a generalisation of Girard's Geomet…
Memoization for Unary Logic Programming: Characterizing PTIME
Clément Aubert, Marc Bagnol, Thomas Seiller
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 pr…