BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Samuel Mimram//Proofs and Algorithms seminar//EN
X-WR-CALNAME:Proofs and Algorithms seminar
BEGIN:VEVENT
SUMMARY:Gabriele Vanoni / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20241209T133000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20241209T143000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.129946551201
DESCRIPTION:Gabriele Vanoni: TBA\n\nTBA\n
LOCATION:room TBA
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alejandro Diaz-Caro / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20241202T133000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20241202T143000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.4700758595
DESCRIPTION:Alejandro Diaz-Caro: TBA\n\nTBA\n
LOCATION:room Grace Hopper
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Loïc Pujet / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20241125T133000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20241125T143000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.365504084966
DESCRIPTION:Loïc Pujet: TBA\n\nTBA\n
LOCATION:room Marcel-Paul Schützenberger
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Louis Lemonnier / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20241112T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20241112T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.388266084197
DESCRIPTION:Louis Lemonnier: A recipe for the semantics of reversible prog
ramming\n\nIn this presentation\, we explore the foundational elements req
uired to interpret reversible programming within a categorical framework.
We use the symmetric pattern-matching language introduced by Sabry\, Valir
on\, and Vizzotto as a reference point\, and we incorporate several improv
ements. We show that inductive data types and recursion can also be effect
ively modelled in this setting. However\, these results do not straightfor
wardly extend to the pure quantum case. We provide insights into the chall
enges encountered and propose potential directions for addressing these li
mitations\, for example with guarded recursion.\n\n(Self) references:\n* [
Classical reversible semantics](https://arxiv.org/abs/2309.12151)\n* [Firs
t-order quantum semantics (chapter 3)](https://arxiv.org/abs/2406.07216)\n
* [Non-cartesian guarded recursion](https://arxiv.org/abs/2409.14591)\n
LOCATION:room Marcel-Paul Schützenberger
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Yorgo Chamoun / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20241106T143000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20241106T153000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.607657507431
DESCRIPTION:Yorgo Chamoun: De Morgan toposes and model theory\n\nDe Morgan
's law\, also known as "weak excluded middle"\, is expressed in a Heyting
algebra (hence in intuitionistic logic) by the equality ¬x ∨ ¬¬x = 1
for any element x of the algebra. On the other hand\, a topos is a "pastic
he" category of the category of sets\, and therefore admits an internal la
nguage that is at least intuitionistic. We can therefore naturally define
a De Morgan topos as a topos whose internal logic admits De Morgan's law\,
but an "external" approach\, without any mention of the internal logic\,
is possible and is very practical to handle. The aim of this presentation
will be to illustrate different facets of these toposes\, adopting this ex
ternal approach. Firstly\, we will attempt to establish links with model t
heory and\, more specifically\, the amalgamation property\, via the notion
of classifying topos of a geometric theory. Secondly\, we will show how a
De Morgan topos can be associated in a more or less canonical way with an
y topos\, and the contributions in this field of the tools recently introd
uced by Caramello for studying (among other things) the internal locales o
f a topos.\n
LOCATION:room Philippe Flajolet
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dominik Kirst / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20241104T133000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20241104T143000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.282476306156
DESCRIPTION:Dominik Kirst: Mechanised Constructive Reverse Mathematics: Th
e Examples of Completeness\, Löwenheim-Skolem Theorems\, and Post's Probl
em\n\nThe idea of (constructive) reverse mathematics is to identify natura
l (sub-classical) axioms that are equivalent to certain mathematical theor
ems and therefore characterise their logical strength. Especially in the c
onstructive case\, this research programme highly depends on the choice of
base theory\, for which we employ the calculus of inductive constructions
\, and benefits from mechanisation\, for which we use the Coq proof assist
ant.\n\nIn this talk\, I will give an overview of some ongoing projects co
ncerning Gödel's completeness theorem for first-order logic\, the related
Löwenheim-Skolem theorems\, as well as Post's problem concerning the exi
stence of a semi-decidable yet undecidable Turing degree strictly below th
e halting problem. Especially the latter exploits a synthetic approach to
computability theory available in any constructive foundation\, where the
reference to an explicit model of computation can be disposed of by simply
considering every function to be computable.\n
LOCATION:room Marcel-Paul Schützenberger
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alexis Saurin / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20241014T133000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20241014T143000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.689616641717
DESCRIPTION:Alexis Saurin: Craig-Lyndon interpolation as cut-introduction
and its computational content\n\nAfter Craig’s seminal results on interp
olation theorem\, a number and variety of proof-techniques\, be they seman
tical or proof-theoretical\, have been designed to establish interpolation
theorems. Among them\, Maehara’s method is specific due to its applicab
ility to a wide range of logics admitting cut-free complete proof systems.
\n\nBy reconsidering Maehara’s method\, I will show how one can extract
a “proof-relevant” interpolation theorem for first-order linear-logic
stated as follows: if π is a cut-free proof of A⊢B\, we can find (i) a
formula C in the common vocabulary of A and B and (ii) proofs π1 of A⊢C
and π2 of C⊢B the proof π′ of A⊢B\, obtained by cutting π1 with
π2 on C\, normalizes to π by cut-reduction.\n\nI will carry out this inv
estigation of proof-relevant interpolation in two frameworks:\n\nFirst\, i
n the traditional sequent calculus\, I will show that interpolation can be
organized in two phases:\n(i) a bottom-up phase which decorates the seque
nts with a so-called splitting followed by\n(ii) a top-down phase which so
lves the interpolation problem\, synthesizing the interpolant by cut-intro
duction.\nThe flexibility of the approach is exploited to carry the interp
olation-as-cut-introduction to classical and intuitionistic logics\, satis
fying Craig as well as Lyndon's constraints on the vocabulary of the inter
polant.\n\nThen\, I will move to Curien & Herbelin's duality of computatio
n framework and prove a computational version of the above result in Syste
m L. The computational content of Maehara's interpolation can therefore be
understood as the factorization of a computation into a term and an evalu
ation context which interact through an interface-type\, the interpolant.\
n\nAfter discussing how the result relates to a proof-relevant refinement
of Prawitz’ proof of the interpolation theorem in natural deduction disc
overed by Čubrić in the 90’s for the simply typed λ-calculus\, I will
explain -- depending on time and interest of the audience -- how this app
roach extends to proof-nets\, expoiting the correctness criteria\, and to
circular proofs in logics with fixed-points.\n
LOCATION:room Henri Poincaré
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Bruno Drieux / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20241007T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20241007T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.298359633351
DESCRIPTION:Bruno Drieux: Catégories syntactiques pour le produit tensori
el des motifs de Nori\n\nSuivant l'idée originale de Nori\, nous proposon
s une construction\, basée sur la logique catégorielle\, d'une catégori
e abélienne monoïdale symétrique universelle associée à une représen
tation d'un carquois dans une catégorie d'espaces vectoriels. Nous étudi
ons ensuite la relation entre cette construction et la généralisation de
la construction de Nori afin d'établir des critères explicites d'existe
nce de structures sur cette dernière. Nous obtenons en particulier une co
nstruction alternative du produit tensoriel des motifs mixtes de Nori. \n
LOCATION:room Marcel-Paul Schützenberger
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Victoria Barrett / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240930T133000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240930T143000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.0310156944126
DESCRIPTION:Victoria Barrett: A strictly linear system for propositional c
lassical logic\n\nWe present a proof system for a conservative extension o
f propositional classical logic with decision trees that is strictly linea
r\, based on recent work in subatomic logic. This means that not only ther
e are no structural rules such as contraction and weakening but there are
no rules for unit equalities either\, and there is no negation. Yet\, its
classical semantics and proof-theoretic properties can be recovered via an
interpretation map at a polynomial cost. Moreover\, this system can p-sim
ulate substitution Frege. Those results are made possible primarily by two
technical advances: 1) an ‘Eversion Lemma’\, that guarantees extreme
flexibility in manipulating formulae to match a given logical context\, an
d 2) a form of explicit substitution for derivations into derivations. We
argue that this proof system represents a significant step towards a notio
n of factorisation for proofs. That will hopefully lead us to a semantics
of proofs adequate to solve the proof identity problem.\n
LOCATION:room Marcel-Paul Schützenberger
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andrei Paskevich / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240924T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240924T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.708666518874
DESCRIPTION:Andrei Paskevich: Coma: an intermediate verification language
with explicit abstraction barriers\n\nComa is a minimalistic algorithmic l
anguage designed for deductive verification. It adopts the continuation-pa
ssing style which allows us to express in a natural manner the standard co
ntrol structures — conditionals\, loops\, subroutine calls\, and excepti
on handling — using only three elementary constructions.\n\nThe specific
ation annotations in Coma take the form of assertions mixed with the rest
of the program code. A special barrier tag is used to separate\, inside a
subroutine definition\, the "interface" part of the code\, which should be
verified at each call\, from the "implementation" part\, which is verifie
d only once\, for all possible inputs. In comparison with traditional cont
ract-based specification\, this offers us an additional degree of freedom\
, as we can provide separate specification for different execution paths i
n the code. We can also forgo the barriers entirely for some (or all) of t
he paths\, which effectively inlines the corresponding code during the com
putation of verification conditions.\n\nVerification conditions for Coma p
rograms are structurally similar to what is generated by the classical wea
kest-precondition calculus. However\, our procedure can also factorize the
instances of selected subformulas in the resulting proof obligation\, whi
ch leads to more compact verification conditions in the style of Flanagan
and Saxe.\n
LOCATION:room Philippe Flajolet
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ryoma Sin'ya / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240913T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240913T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.848846380062
DESCRIPTION:Ryoma Sin'ya: Measure Theoretic Approach to Formal Languages\n
\nA language L is said to be regular measurable if there exists an infinit
e sequence of regular languages that “converges” to L. This notion was
introduced by the speaker in 2021 and used for classifying non-regular la
nguages by using regular languages. In this talk\, we describe why this no
tion was introduced\, and give a brief overview of decidability results re
lating to the measurability on subclasses (local subvarieties) of regular
languages\, eg.\, star-free\, generalised definite\, piecewise-testable\,
and group languages.\n
LOCATION:room Marcel-Paul Schützenberger
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Denis Antipov / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240627T160000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240627T170000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.915111666858
DESCRIPTION:Denis Antipov: Theoretical Foundations of Evolutionary Diversi
ty Optimisation for Multi-objective Problems.\n\nIn practical optimisation
problems there is often a risk that the best found solutions turn out inf
easible for a range of reasons. To avoid the need to re-run optimisation a
lgorithms once such situations occur\, it is common to look for a diverse
set of good solutions\, since the diversity minimises the chances that all
of them turn out to be infeasible. This is a much more challenging task\,
since we perform the search in the space of (multi-)sets of solutions\, w
hich significantly increases the dimensionality of the problem compared to
the regular optimisation. The evolutionary algorithms (EAs) are well-suit
ed for this task\, since they are naturally designed to optimise populatio
ns. This approach of using EAs to evolve diverse populations is called evo
lutionary diversity optimisation (EDO). It was shown to be effective in pr
actice\, but the process of EDO (and therefore\, the most effective approa
ches to it) is not well-understood. In this talk we will discuss the (few)
theoretical results which exist in this field\, focusing mainly on EDO in
Multi-objective domain.\n
LOCATION:room Marcel-Paul Schützenberger
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jui-Hsuan Wu / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240613T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240613T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.0187638220917
DESCRIPTION:Jui-Hsuan Wu: Positive Focusing is Directly Useful\n\nRecently
\, Miller and I introduced the positive λ-calculus\, a call-by-value λ-c
alculus with sharing obtained by assigning proof terms to the positively p
olarized focused proofs for the implicational fragment of Gentzen’s LJ.
The positive λ-calculus stands out among λ-calculi with sharing for a co
mpactness property related to the sharing of variables. In this talk\, I w
ill show that—thanks to compactness—the positive calculus neatly captu
res the core of useful sharing\, a technique for the study of reasonable t
ime cost models.\n\nThis is joint work with Beniamino Accattoli.\n
LOCATION:room Marcel-Paul Schützenberger
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ernest van Wijland / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240527T160000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240527T170000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.170557633438
DESCRIPTION:Ernest van Wijland: Faster Approximation Scheme for Euclidean
k-TSP\n\nIn the Euclidean $k$-traveling salesman problem ($k$-TSP)\, we ar
e given $n$ points in the $d$-dimensional Euclidean space\, for some fixed
constant $d>2$\, and a positive integer $k$. The goal is to find a shorte
st tour visiting at least $k$ points. We give an approximation scheme for
the Euclidean $k$-TSP in time $n.2^{O(1/\\varepsilon^{d-1})}.(\\log n)^{2d
^2\\cdot 2^d}$. This improves Arora's approximation scheme of running time
$n.k(\\log n)^{\\left(O\\left(\\sqrt{d}/\\varepsilon\\right)\\right)^{d-1
}}$ [J. ACM 1998]. Our algorithm is Gap-ETH tight and can be derandomized
by increasing the running time by a factor $O(n^d)$. This is joint work wi
th Hang Zhou. This work was accepted for publication at the International
Symposium on Computational Geometry (SoCG)\, 2024.\n
LOCATION:room Emmy Noether
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Thomas Debris-Alazard / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240522T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240522T113000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.360629659562
DESCRIPTION:Thomas Debris-Alazard: An Example of Quantum Oblivious Computa
tion\n\n
LOCATION:room Philippe Flajolet
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Yuliy Baryshnikov / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240529T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240529T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.199112542524
DESCRIPTION:Yuliy Baryshnikov: Spaces of Obstacle Avoiding Paths\n\nA broa
d class of models deal with spaces of directed paths avoiding some dynamic
obstacles. (Examples include concurrency\, in computer science\, and coll
ision avoidance in control theory.) The topology (say\, the homotopy type)
of these spaces is not yet well understood.\n\nIt turns out\, the study o
f these spaces is in many respects parallel to the theory of linear subspa
ce arrangements. I will outline some recent results\, and the key tools us
ed to obtain them\, - in particular\, the apparatus of diagrams of spaces.
\n
LOCATION:room Grace Hopper
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Thomas Seiller / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240515T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240515T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.539202060724
DESCRIPTION:Thomas Seiller: Mathematical informatics\n\nWhat 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 an
swer these questions. Indeed\, it is a mathematical theory of computable f
unctions\, and does not account for computation itself. A symptomatic cons
equence is the notion of Turing-completeness. This standard (sole?) equiva
lence between models of computation is purely extensional: it does only ca
re about what is computed and not how\, blind to complexity aspects and th
e question of algorithmic completeness. More importantly\, the theory of c
omputation is continuously growing further from how actual machines comput
e. I will 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 w
ill argue that it generalises computability theory while still allowing to
recover standard results.\n\nIf time permits\, I can then explain how thi
s theory can be used to (I will let he audience decide which items will be
discussed):\n\n* provide a uniform account of several lower bounds from a
lgebraic complexity and strengthen them\n* define static analysis methods
which can be implemented in usable tools\n* define families of linear real
isability models (realisability models for linear logic)\n* lead to a sema
ntic approach of implicit computational complexity\n* propose a formal def
inition of the notion of algorithm\n
LOCATION:room Grace Hopper
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Vikraman Choudhury / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240426T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240426T113000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.98389370134
DESCRIPTION:Vikraman Choudhury: Symmetries in constructive mathematics\n\n
I this talk\, I will discuss the constructive theory of free commutative m
onoids (or finite multisets)\, and free symmetric monoidal groupoids\, in
Univalent Foundations. I will show several applications to computer scienc
e: axiomatics of sorting algorithms\, differential structure in models of
linear logic\, and axiomatisation of type isomorphisms in a language for r
eversible computing.\n
LOCATION:room Philippe Flajolet
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Serge Lechenne / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240424T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240424T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.570191857833
DESCRIPTION:Serge Lechenne: Categorical structure in combinatorial algebra
s\n\nWe investigate a class of combinatory algebras\, called ribbon combin
atory algebras\, in which we can interpret both the braided untyped linear
lambda calculus and framed oriented tangles. Any reflexive object in a ri
bbon category gives rise to a ribbon combinatory algebra. Conversely\, Fro
m a ribbon combinatory algebra we can construct a ribbon category with a r
eflexive object\, from which the combinatory algebra can be recovered. To
show this\, and also to give the equational characterization of ribbon com
binatory algebras\, we make use of the internal PRO construction developed
in Hasegawa’s recent work. Interestingly\, we can characterize ribbon c
ombinatory algebras in two different ways: as balanced combinatory algebra
s with a trace combinator\, and as balanced combinatory algebras with dual
ity.\n
LOCATION:room Philippe Flajolet
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Miki Hermann / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240327T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240327T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.1372468129
DESCRIPTION:Miki Hermann: Primal Grammars Driven Automated Induction\n\nAu
tomated induction is important for many computer sciences and artificial i
ntelligence applications. However\, proof by induction is undecidable and
diverges even for small examples\, leading to failures in the proving expe
rience.\n\nMany techniques have proposed ad-hoc heuristics to speculate on
additional lemmas that hopefully stop the divergence. Although these meth
ods have succeeded in proving interesting theorems\, they have significant
limitations: in particular\, they often fail to find appropriate lemmas\,
and the provided lemmas may not be valid.\n\nWe present a new technique t
hat allows us to perform inductive proofs in conditional theories by autom
atically detecting the divergence of proof traces and deriving a primal gr
ammar as well as new lemmas that schematize the divergent sequences and\,
thus\, allow breaking the divergence and ending the proof. Our new techniq
ue is presented as a set of inference rules whose soundness and refutation
al completeness have been formally proved. Refutational completeness is pa
rticularly useful for detecting flaws in critical systems. Moreover\, unli
ke related work\, our new technique has no risk of over-generalization. If
the initial conjectures are valid\, then the lemmas generated by our tech
nique subsume the divergent sequence and are also valid.\n\nThe cornerston
e of our method is the use of primal grammars\, which are based on primiti
ve recursive functions and represent the most general decidable schematiza
tion\, with respect to description power\, among all known schematizations
. Our technique always succeeds in building a primal grammar when the dive
rgence follows a primitive recursive pattern\; this allows us to cover a l
arge class of problems.\n\nOur new technique has been implemented in C++ a
nd successfully proved several dozens of complex examples that fail with w
ell-known theorem provers such as ACL2\, Isabelle\, LEAN\, PVS\, RRL\, SPI
KE\, and related techniques for capturing and schematizing divergence for
proof by induction.\n
LOCATION:room Grace Hopper
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Inigo Incer / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240314T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240314T160000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.990453959327
DESCRIPTION:Inigo Incer: Towards Provably Safe and Secure Systems with Con
tract-Based Design\n\nThe task of system design is shared by all engineeri
ng disciplines\, each\ncoming with its own techniques. In spite of their d
ifferences in tools\,\nthere is large intersection in their conceptual app
roach to design. In this\ntalk\, we exploit this commonality to take an ab
stract view of systems and\ntheir composition. We understand systems and s
ubsystems in terms of their\nassume-guarantee specifications\, or contract
s.\n\nAssume-guarantee contracts are formal specifications that state (i)
the\nassumptions that a design element makes on its environment and (ii) t
he\nguarantees it delivers when the environment behaves according to the\n
contract's assumptions. Contracts come with a rich algebra that allows us
to\ncarry out several design-relevant tasks: obtaining system-level\nspeci
fications from component specifications\, finding specifications of\ncompo
nents that need to be added to a design in order to meet an objective\,\ne
tc. We will introduce the algebra of contracts and discuss how the various
\nalgebraic operations relate to system-design tasks. We will discuss\nhyp
ercontracts\, an extension of assume-guarantee reasoning to support the\nf
ormal analysis of key security and robustness properties. We will also\ndi
scuss the application of this methodology and Pacti\, a software package\n
that supports system design using contracts\, in applications ranging from
\nspace-mission design to synthetic biology.\n\nBio: Inigo Incer is a post
doctoral researcher at Caltech and UC Berkeley. He\nobtained his PhD from
UC Berkeley in 2022 under the guidance of Alberto\nSangiovanni-Vincentelli
. He is interested in all aspects of cyber-physical\nsystems\, emphasizing
formal methods and AI that support their compositional\ndesign and analys
is. Before pursuing a PhD\, Inigo was an IC designer in\nAustin. His work
has been supported by the NSF/ASEE eFellows program and the\nUC Berkeley C
hancellor's Fellowship.\n
LOCATION:room Marcel-Paul Schützenberger
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Fabio Gadducci / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240313T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240313T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.348387309681
DESCRIPTION:Fabio Gadducci: Petri nets\, monoidal categories\, and linear
logic (A survey and some recent results)\n\nIn a seminal paper Montanari a
nd Meseguer have shown that an algebraic interpretation of Petri nets in t
erms of monoids can be used to provide an elegant characterisation of the
deterministic computations of a net\, accounting for their sequential and
parallel composition\, in terms of monoidal categories. The same framework
was recognised by Asperti as the right one for interpreting the multiplic
ative fragment of linear logic. In this talk we will give a survey of thes
e classical results\, plus adding a novel characterisation for non-determi
nistic computations of a net in terms of dioidal categories\, which are th
e categorical equivalent of tropical semirings\, and suggesting a possible
connection with the multiplicative additive fragment of linear logic.\n
LOCATION:room Grace Hopper
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Damiano Mazza / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240228T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240228T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.460509180087
DESCRIPTION:Damiano Mazza: A Categorical Approach to Describing Complexity
Classes\n\nWe introduce a categorical framework for describing decision p
roblems\nand providing machine-independent characterizations of complexity
\nclasses\, mixing ideas coming from descriptive complexity and categorica
l\nlogic. The framework is based on the opposite of the category of small
\nBoolean lextensive categories and logical functors. This has nice\ncate
gorical properties and\, crucially\, its morphisms may be seen as\ndescrip
tions of decision problems. The complexity of problems may be\ncontrolled
by restricting morphisms via suitable algebraic and logical\nproperties\,
obtaining several well-known classes (recursively enumerable\nproblems\,
NP\, P\, NL\, P/poly...). If time permits\, we will see how this\napproac
h leads to considering algebraic objects which generalize\ncommutative rin
gs and affine schemes (in the sense of algebraic geometry).\n
LOCATION:room Philippe Flajolet
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Noam Zeilberger / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240215T104500
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240215T114500
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.025111265105
DESCRIPTION:Noam Zeilberger: Context-free grammars and finite-state automa
ta over categories\n\nA little over a year and a half ago\, Paul-André Me
lliès and I wrote [a paper](https://doi.org/10.46298/entics.10508) giving
a categorical analysis of the so-called Chomsky–Schützenberger represe
ntation theorem\, whose usual formulation states that "a language is conte
xt-free iff it is a homomorphic image of the intersection of a Dyck langua
ge with a regular language". Since then\, our understanding of the materia
l has evolved significantly\, and we wrote a thoroughly revised and expand
ed version of the paper: [_The categorical contours of the Chomsky-Schütz
enberger representation theorem_](https://inria.hal.science/hal-04399404).
\n\nThe main message of the paper is that there are natural notions of "co
ntext-free grammar" and of "non-deterministic finite state automaton" over
arbitrary categories and operads\, and that looking at CFGs and NDFAs in
this way seems to have some real explanatory power. In the talk I will giv
e some examples\, and sketch some of the other ideas and results from the
paper.\n
LOCATION:room Marcel-Paul Schützenberger
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Benedikt Ahrens / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240207T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240207T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.840337873853
DESCRIPTION:Benedikt Ahrens: Univalent foundations for the formalization o
f (higher) category theory\n\nCategory theory is a mathematical theory of
structures and their\ninteractions. It was originally developed to axiomat
ize algebraic\ntopology\; in the meantime\, it has proved useful as a lang
uage and\ninfrastructure for organizing knowledge in many areas of mathema
tics\,\ncomputer science\, data science\, biology\, and more.\n\nThe formu
lation of category theory in set-theoretic foundations has been\nseen as p
roblematic: the notion of "sameness" between mathematical\nobjects provide
d by set theory does not coincide with the fundamental\nnotion of isomorph
ism in category theory. This divergence is exacerbated\nwhen considering h
igher-categorical structures\, such as categories\nthemselves.\n\nIn this
talk\, we explain how univalent foundations provides exactly the\nright se
tting in which to formalize category theory. In particular\,\nequivalence
of categories coincides with "sameness" of categories in the\nsense of uni
valent foundations.\n
LOCATION:room Grace Hopper
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Hang Zhou / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240131T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240131T113000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.220287048292
DESCRIPTION:Hang Zhou: Capacitated Vehicle Routing\n\nIn the capacitated v
ehicle routing problem\, we are given a metric space with a vertex called
depot and a set of vertices called terminals. The goal is to find a minimu
m length collection of tours starting and ending at the depot such that ea
ch tour visits at most k terminals\, and each terminal is visited by some
tour. In this talk\, I am going to talk about recent progress on the capac
itated vehicle routing problem on trees and in the two-dimensional Euclide
an plane.\n
LOCATION:room Philippe Flajolet
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Emmanuel Haucourt / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240125T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240125T160000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.249222281379
DESCRIPTION:Emmanuel Haucourt: Smooth models of concurrent programs\n\nA s
equential program is usually represented by an automaton\, i.e. a graph la
belled with instructions on which the instruction pointer moves. There is
no such consensus about the way of representing concurrent programs. Highe
r dimensional automata were introduced to this end by Pratt and van Glabbe
ek in the early 90's\, the first continuous models were proposed by Fajstr
up\, Goubault and Raussen about a decade later\, mixing topology and (loca
l) order. As we will explain during the talk\, the two later derive from a
non-Hausdorff manifold M equipped with a parallelization (i.e. a tuple of
vector fields (f₁\,…\,fₙ) giving a basis of the tangent space at ea
ch point of the manifold). The manifold M even comes with an atlas whose t
ransition functions are mere vector translations\; concretely\, it means t
hat one can do differential calculus on M (almost) as in the euclidean spa
ce ℝⁿ\, i.e. without paying attention to charts.\n
LOCATION:room Marcel-Paul Schützenberger
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Matthew di Meglio / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20240117T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20240117T160000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.3517467117
DESCRIPTION:Matthew di Meglio: Enriched bisimulations\n\n(Joint work with
Bryce Clarke)\n\nBisimulations of Kripke frames\, and strong and weak bisi
mulations of labelled transition systems\, are all examples of a more gene
ral notion of bisimulation for enriched graphs and enriched categories. I
will give a gentle and example-oriented introduction to enriched categorie
s\, their bisimulations\, and the connection to enriched lenses. We hope t
hat this talk will lead to discussion on further aspects of the theory of
Kripke frames and modal logic that could be generalised to the setting of
enriched categories.\n
LOCATION:room (online)
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Vladik Kreinovich / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20231221T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20231221T113000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.669240304549
DESCRIPTION:Vladik Kreinovich: Deep Learning (Partly) Demystified\n\nSucce
sses of deep learning are partly due to appropriate selection of activatio
n function\, pooling functions\, etc. Most of these choices have been made
based on empirical comparison and heuristic ideas. In this talk\, we show
that many of these choices -- and the surprising success of deep learning
in the first place -- can be explained by reasonably simple and natural m
athematics.\n
LOCATION:room Philippe Flajolet
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Meven Lennon-Bertrand / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20231212T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20231212T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.937722436839
DESCRIPTION:Meven Lennon-Bertrand: Towards a certified proof assistant ker
nel – What it takes and what we have\n\nProof assistant kernels are a na
tural target for program certification: they are small\, critical\, and we
ll-specified. Still\, despite the maturity of the field of software certif
ication\, we are yet to see a certified Agda\, Coq or Lean. In this talk\,
I will try and explain why this is not such an easy task\, and present tw
o complementary projects going in that direction. The first\, MetaCoq\, is
a large scale project\, broadly aiming at giving tools to manipulate Coq
terms and derivations inside of Coq\, in particular developing an importan
t body of formalized proofs around Coq's typing. The second is a more rece
nt endeavour\, aimed at tackling the mother of all properties: normalisati
on.\n
LOCATION:room Nicolaas Govert de Bruijn (salle 34\, rez-de-chaussée)
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Federico Olimpieri / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20231206T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20231206T160000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.924460614614
DESCRIPTION:Federico Olimpieri: Why are proofs relevant in proof relevant
models?\n\nRelational models of λ-calculus can be presented as type syste
ms\, the relational interpretation of a λ-term being given by the set of
its typings. Within a distributors-induced bicategorical semantics general
izing the relational one\, we identify the class of ‘categorified’ gra
ph models and show that they can be presented as type systems as well. We
prove that all the models living in this class satisfy an Approximation Th
eorem stating that the interpretation of a program corresponds to the filt
ered colimit of the denotations of its approximants. As in the relational
case\, the quantitative nature of our models allows to prove this property
via a simple induction\, rather than using impredicative techniques. Unli
ke relational models\, our 2-dimensional graph models are also proof-relev
ant in the sense that the interpretation of a λ-term does not contain onl
y its typings\, but the whole type derivations. The additional information
carried by a type derivation permits to reconstruct an approximant having
the same type in the same environment. From this\, we obtain the characte
rization of the theory induced by the categorified graph models as a simpl
e corollary of the Approximation Theorem: two λ-terms have isomorphic int
erpretations exactly when their B'ohm trees coincide.\n
LOCATION:room Philippe Flajolet
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sergio Rajsbaum / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20231130T113000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20231130T123000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.46923988414
DESCRIPTION:Sergio Rajsbaum: The origins of blockchains: milestones of cry
ptography\, distributed systems and databases\n\nBlockchains have served a
s decentralized platforms to transform the way we think about databases\,
distributed systems and finance in a world where people can interact with
out knowing each other and across borders without government intermediarie
s. Nevertheless\, an historic perspective of the ideas that brought us her
e can be traced back to the birth of decentralized systems in the 1970s wi
th roots coming from research in cryptography\, distributed systems and da
tabases. A fascinating history where new notions were invented along the w
ay\, requiring the design of new algorithms\, and the understanding of sci
entific principles about what can and cannot be done by a collection of co
mputers communicating with each other.\n
LOCATION:room Amphi Sophie Germain\, Batiment Turing
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Khalil Ghorbal / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20231124T100000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20231124T110000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.625159555852
DESCRIPTION:Khalil Ghorbal: Linear Hybrid Systems are Hard: The Case of Li
near Complementarity Systems and The Quest For Characterizing Q-matrices\n
\nLinear complementarity systems (LCS) form a special class of linear hybr
id systems with an exponential number of modes and a linear differential a
lgebraic equation in each mode. While seemingly simple\, little is known a
bout the existence (and uniqueness) of continuous solutions for LCS. The o
nly known sufficient condition is rather strong and requires the existence
and uniqueness of solutions for the underlying linear complementarity pro
blem (LCP) which\, for a fixed matrix M and a given vector q\, asks whethe
r there exists a pair of vectors (w\,z) satisfying w - M z = q\, w\,z ≥
0\, and w·z = 0. M is said to be a Q-matrix when a solution exists for al
l q. We start by exposing the inherent difficulty of characterizing Q-matr
ices by reformulating the problem as a covering problem of Rⁿ. We then i
nvestigate the regions where no solution exists (so called holes) and show
that they only occur in specific locations. This property is exploited to
fully characterize planar and spatial Q-matrices via a local reduction ar
ound the vectors defining the problem.\n\nThis is a joint work with Christ
elle Kozaily.\n
LOCATION:room Grace Hopper
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Luc Jaulin / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20231110T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20231110T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.00409628655472
DESCRIPTION:Luc Jaulin: Guaranteed numerical methods to secure a zone with
autonomous robots\n\nIn this talk\, we provide an interval-based method t
o prove that there are no submarine intruders inside a zone of the ocean (
here the Bay of Biscay). For this purpose\, a group of underwater robots w
ill be used. We assume that\n\n- Our robots are able to localize themselve
s with a given accuracy.\n- They are able to communicate at a low rate at
low distances.\n- Each robot is able to detect any intruder inside a disk
of a known radius.\n- The speed of the intruders is assumed to be bounded
and is small with respect to that of our robots.\n\nOur goal is twofold:\n
\n- to characterize a set for which we can guarantee that there is no intr
uder (this corresponds to the secure zone)\n- to find a control strategy f
or the group of robots in order to extend the secure zone as much as possi
ble.\n
LOCATION:room Grace Hopper
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:James Hefford / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20231030T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20231030T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.930775404939
DESCRIPTION:James Hefford: Holes in Monoidal and Premonoidal Categories\n\
nThe category of holes or "optics" in monoidal categories dates back to th
e work of Pastro and Street who built on the study of profunctors with str
ength due to Tambara. These optics have come to be understood as a unifyin
g language for describing various bidirectional data accessors. In this ta
lk I will discuss the sequential and parallel composition of optics and ho
w this can be seen to arise from a produoidal structure on the category of
optics. This was first noticed by Garner and López Franco but seems ofte
n to have been neglected in applications.\n\nOptics have also been conside
red over actegories - categories equipped with an action by a monoidal cat
egory - giving rise to "mixed" optics. Premonoidal categories are a partic
ularly interesting case of actegories since they often arise in the modell
ing of computational side-effects. I will discuss the structure of optics
over a premonoidal base and the sequential and parallel composition of suc
h optics. In particular\, one of the monoidal-like structures of this cate
gory requires a generalisation of premonoidal categories to their non-repr
esentable cousins\, analogous to the generalisation from monoidal to promo
noidal categories.\n\nThis talk is based on joint work with Mario Román a
nd Matt Earnshaw.\n
LOCATION:room Grace Hopper
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Éric Goubault / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20231017T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20231017T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.664246161261
DESCRIPTION:Éric Goubault: Directed homology and persistence modules\n\nI
n this talk\, we will try to give a self-contained account on a constructi
on for a directed homology theory based on modules over algebras\, linking
it to both persistence homology and natural homology.\n\nPersistence modu
les have been introduced originally for topological data analysis\, where
the data set seen at different « resolutions » is organized as a filtra
tion of spaces. This has been further generalized to multidimensional pers
istence and « generalized » persistence\, where a persistence module was
defined to be any functor from a partially ordered set\, or more generall
y a preordered set\, to an arbitrary category (in general\, a category of
vector spaces). \n\nDirected topology has its roots in a very different ap
plication area\, concurrency and distributed systems theory rather than da
ta analysis. Its goal is to study (multi-dimensional) dynamical systems\,
discrete (precubical sets\, for application to concurrency theory) or cont
inuous time (differential inclusions\, for e.g. applications in control)\,
that appear in the study of multi-agent systems. In this framework\, topo
logical spaces are « directed »\, meaning they have « preferred direc
tions »\, for instance a cone in the tangent space\, if we are considerin
g a manifold\, or the canonical local coordinate system in a precubical se
t. Natural homology\, an invariant for directed topology\, defines a natur
al system of modules\, a further categorical generalization of (bi)modules
\, describing the evolution of the standard (simplicial\, or singular) hom
ology of certain path spaces\, along their endpoints. Indeed\, this is\, i
n spirit\, similar to persistence homology.\n\nThis talk will be concerned
with a more « classical » construction of directed homology\, mostly fo
r precubical sets here\, based on (bi)modules over (path) algebras\, makin
g it closer to classical homology with value in modules over rings\, and o
f the techniques introduced for persistence modules. Still\, this construc
tion retains the essential information that natural homology is unveiling.
Of particular interest will be the role of restriction and extension of s
calars functors\, that will be central to the discussion of Kunneth formul
as and relative homology sequences. If time permits as well\, we will disc
uss some « tameness » issues\, for dealing with practical calculations.\
n
LOCATION:room Grace Hopper
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Gabriel Scherer / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20231016T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20231016T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.0598576070428
DESCRIPTION:Gabriel Scherer: Constructor unboxing\n\nIn this work I will p
resent a new feature proposed for the OCaml programming language\, "constr
uctor unboxing"\, first suggested by Jeremy Yallop in March 2020. It enabl
es a more efficient representation of certain sum types\, but requires a s
tatic analysis to forbid certain unboxing requests that would be unsound.\
n\nTo define this static analysis\, one has to solve a problem of normaliz
ation of first-order definitions in presence of recursion. In the talk I h
ope to explain my current understanding of this halting problem\, and pres
ent an algorithm to compute normal forms and reject (in finite time) non-n
ormalizable definitions.\n
LOCATION:room Marcel-Paul Schützenberger
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Brigitte Pientka / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20230925T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20230925T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.870937085886
DESCRIPTION:Brigitte Pientka: Mechanizing Session-Types Using a Structural
View — Enforcing linearity without linearity\n\nSession types employ
a linear type system that ensures that communication channels cannot be im
plicitly copied or discarded. As a result\, many mechanizations of these s
ystems require modeling channel contexts and carefully ensuring that they
treat channels linearly. We demonstrate a technique that localizes lineari
ty conditions as additional predicates embedded within type judgments\, wh
ich allows us to use structural typing contexts instead of linear ones. Th
is technique is especially relevant when leveraging (weak) higher-order ab
stract syntax to handle channel mobility and the intricate binding structu
res that arise in session typed systems.\n\nFollowing this approach\, we m
echanize a session-typed system based on classical linear logic and its ty
pe preservation proof in the proof assistant Beluga\, which uses the logic
al framework LF as its encoding language. We also prove adequacy for our e
ncoding. This shows the tractability and effectiveness of our approach in
modelling substructural systems such as session-typed languages.\n
LOCATION:room Grace Hopper
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Mirai Ikebuchi / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20230920T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20230920T160000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.529488739191
DESCRIPTION:Mirai Ikebuchi: Applications of Homological Algebra to Algebra
ic Theories\n\nIt is well-known that some algebraic theories such as group
s or Boolean algebras can be defined by fewer equational axioms than the o
riginal axioms. However\, it is not easy to determine if a given set of ax
ioms is the smallest or not. Malbos and Mimram investigated a general meth
od to find a lower bound of the cardinality of the set of equational axiom
s (or rewrite rules) that is equivalent to a given algebraic theory (or te
rm rewriting system)\, using homological algebra. In this talk\, I develop
the homology theory for term rewriting systems more and provide a better
lower bound under the constraint that the set of function symbols is fixed
.\nAlso\, the same methodology applies to equational unification\, the pro
blem of solving an equation modulo equational axioms. I provide a relation
ship between equational unification and homological algebra for algebraic
theories: Equational unifiability implies the surjectivity of a homomorphi
sm of abelian groups associated with the algebraic theory and the equation
to solve.\n
LOCATION:room Grace Hopper
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sayan Mitra / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20230711T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20230711T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.793408975184
DESCRIPTION:Sayan Mitra: Optimal Runtime Assurance\n\nA runtime assurance
system (RTA) enables the exercise of an untrusted controller while assurin
g safety with a backup (or safety) controller. The relevant computational
design problem is to create a logic that assures safety by switching to th
e safety controller as needed\, while maximizing some performance criteria
\, such as the utilization of the untrusted controller. Existing RTA desig
n strategies are well-known to be overly conservative and\, in principle\,
can lead to safety violations. In this talk\, I will discuss a formulatio
n of the optimal RTA design problem and present a new approach for solving
it. The approach relies on reward shaping and reinforcement learning. It
can guarantee safety and leverage reinforcement learning for scalability.
We have implemented this algorithm and present experimental results compar
ing our approach with state-of-the-art reachability and simulation-based R
TA approaches in a number of scenarios using aircraft models in 3D space w
ith complex safety requirements. Our approach can guarantee safety while i
ncreasing utilization of the experimental controller over existing approac
hes. We also note that changing from safety to reachability is nontrivial
from the point to view of achieving optimal memoryless policies with rewar
d shaping.\n
LOCATION:room Amphi R111\, ENSTA Paris
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Manon Blanc / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20230628T100000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20230628T110000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.928187220806
DESCRIPTION:Manon Blanc: Measuring robustness of dynamical systems. Relati
ng time and space to length and precision\n\nVerification of discrete time
or continuous time dynamical systems is known to be undecidable. However\
, undecidability is known not to hold for robust systems: if robustness is
defined as the fact that the reachability relation is stable under infini
tesimal perturbation\, then decidability holds. Similarly\, while undecid
ability holds for logical formulas over the reals\, it does not when consi
dering delta-undecidability\, i.e. when properties are either true or delt
a-far from being true. We first relate these notions of robustness. Then\,
we extend these statements at the complexity level: When a system is robu
st\, it makes sense to quantify at which level of perturbation a system is
robust. We prove assuming robustness to polynomial perturbation on precis
ion leads to PSPACE and even to a characterization of PSPACE. We prove ass
uming robustness to polynomial perturbation on time or length leads to sim
ilar statements but with PTIME. We also relate this to analogue models of
computation.\n
LOCATION:room Grace Hopper
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dale Miller / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20230621T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20230621T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.481326130912
DESCRIPTION:Dale Miller: A system of inference based on proof search:an ex
tended abstract\n\nGentzen designed his natural deduction proof system to
"come as close as possible to actual reasoning." Indeed\, natural deducti
on proofs closely resemble the static structure of logical reasoning in ma
thematical arguments. However\, different features of inference are compe
lling to capture when one wants to support the process of searching for pr
oofs. PSF (Proof Search Framework) attempts to capture these features nat
urally and directly. The design and metatheory of PSF are presented\, and
its ability to specify a range of proof systems for classical\, intuition
istic\, and linear logic is illustrated. This is a practice talk for my pr
esentation at LICS 2023\, see [the accompanying paper](http://www.lix.poly
technique.fr/Labo/Dale.Miller/papers/lics2023.pdf).\n
LOCATION:https://bbb.inria.fr/alw-vtl-6bb-kk3
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ufuk Topcu / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20230613T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20230613T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.289595683907
DESCRIPTION:Ufuk Topcu: Autonomous systems in the intersection of formal m
ethods\,learning\, and controls\n\nAutonomous systems are emerging as a dr
iving technology for countlessly many applications. Numerous disciplines t
ackle the challenges toward making these systems trustworthy\, adaptable\,
user-friendly\, and economical. On the other hand\, the existing discipli
nary boundaries delay and possibly even obstruct progress. I argue that th
e nonconventional problems that arise in designing and verifying autonomou
s systems require hybrid solutions at the intersection of learning\, forma
l methods\, and controls. I will present examples of such hybrid solutions
in the context of learning in sequential decision-making processes. These
results offer novel means for effectively integrating physics-based\, con
textual\, or structural prior knowledge into data-driven learning algorith
ms. They improve data efficiency by several orders of magnitude and genera
lizability to environments and tasks that the system had not experienced p
reviously. I will conclude with remarks on a few promising future research
directions\n
LOCATION:room Salle Sophie Germain\, LIX\, Bâtiment Alan Turing
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Will Troiani / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20230601T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20230601T160000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.652790223685
DESCRIPTION:Will Troiani: Computation in logic as the splitting of idempot
ents in algebraic geometry\; two models of multiplicative linear logic\n\n
A hypersurface f = 0 in complex affine space is singular if and only if th
ere exists a non-contractible matrix factorization of f (to be defined in
the talk). Matrix factorisations are organised into a bicategory where com
position is defined via a two-step process\, first an infinite model of th
e composite is described\, and then a terminating procedure is followed to
extract a finite presentation. Is this terminating procedure a semantics
of cut-elimination? By considering simple cases\, Daniel Murfet and mysel
f have uncovered two models of multiplicative linear logic\, one in the sp
ace of coordinate rings where cut-elimination corresponds to the celebrate
d Buchberger Algorithm\, and the other in the space of Quantum Error Corre
ction Codes\, where cut-elimination corresponds to quantum error correctio
n. The general picture has led Murfet and myself to postulate that the spl
itting of idempotents has fundamental relevance to the theory of computati
on. This talk defends this proposition.\n
LOCATION:room Philippe Flajolet
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Hugo Paquet / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20230419T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20230419T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.906509727416
DESCRIPTION:Hugo Paquet: From Game Semantics to Species of Structures\n\nI
n this talk I will discuss the connections between two different models fo
r programming languages: a semantics based on games and strategies\, and a
combinatorial semantics based on profunctors and generalized species of s
tructures. A formal comparison is challenging\, because these models provi
de two different representations of effects and resources. For effects\, b
oth models use a linear continuation monad\, but one is polarized while th
e other isn't. For resources\, both models use a linear exponential comon
ad\, but one saturates under resource symmetries\, while the other picks c
anonical representatives for symmetry classes. The main technical result i
s a bicategorical functor from strategies to species of structures. This h
ighlights the key differences\, and can be used to transport results from
one model to the other. This is based on joint work with P. Clairambault a
nd F. Olimpieri.\n
LOCATION:room Philippe Flajolet
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Luidnel Maignan / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20230411T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20230411T160000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.544939970946
DESCRIPTION:Luidnel Maignan: Non Determinism in Spatialized Systems\, Gene
rically\n\nIn my works with Antoine Spicher and Alexandre Fernandez\, we c
onsider an abstraction of space where we only think of it through the way
it limits the knowledge you can have about the state of a system. This is
formalized through a category of object representing something similar to
a knowledge state about the system. In a recent MFCS paper\, we showed tha
t non-determinism is\, in some categorical sense\, a particular case of th
e general definition. We did it on the concrete example of non-determinist
ic Lindenmeyer systems\, and showed how the 2-monad of families is necessa
ry to express this abstraction. For this presentation\, I would also like
to quickly explain how this is related to different categorical constructi
ons: presheaves\, profunctors\, and left fibrational spans.\n
LOCATION:room Philippe Flajolet
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Carl-Fredrik Nyberg Brodda / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20230405T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20230405T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.56585333067
DESCRIPTION:Carl-Fredrik Nyberg Brodda: Monadic rewriting systems and the
word problem\n\nThe word problem for finitely presented groups and semigro
ups is one of the most fundamental problem in all combinatorial algebra. L
anguage-theoretic methods can be used to study it\, which has revealed dee
ps links in group theory between accessible groups\, virtually free groups
\, the geometry of context-free graphs\, and context-free languages. In th
is talk\, I will go over some recent progress on how I have developed thes
e methods and results to semigroup theory\, as well as new techniques I de
veloped in order to reduce such problems to problems about groups. This in
cludes results from the theory of string rewriting systems\, and a non-con
structive -- but highly algebraic -- definition of the class of all contex
t-free languages (or indeed the class of ET0L languages\, indexed language
s\, etc.) via monadic rewriting systems.\n
LOCATION:room Salle Grace Hopper + BBB
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Farzad Jafarrahmani / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20230329T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20230329T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.864196994494
DESCRIPTION:Farzad Jafarrahmani: Polarized Linear Logic with Fixpoints\n\n
In this talk\, I will present a joint work with Thomas Ehrhard and Alexis
Saurin on μLLP\, which can be viewed both as an extension of Laurent’s
Polarized Linear Logic\, LLP\, with least and greatest fixpoints\, and as
a polarized version of Baelde and Miller’s Linear Logic with fixpoints (
μMALL and μLL). We take advantage of the implicit structural rules of μ
LLP to introduce a term syntax for this language\, in the spirit of the cl
assical lambda-calculus and of system L in the style of Curien\, Herbelin
and Munch-Maccagnoni. We equip this language with a deterministic reductio
n semantics as well as a denotational semantics based on the notion of non
-uniform totality spaces and the notion of categorical model for linear lo
gic with fixpoint. At the end\, I will show you an adequacy result for μL
LP between these operational and denotational semantics\, from which we de
rive a normalization property for μLLP thanks to the properties of the to
tality interpretation.\n
LOCATION:room Philippe Flajolet
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Philipp Fischbeck / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20230316T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20230316T113000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.453683375189
DESCRIPTION:Philipp Fischbeck: On the External Validity of Average-Case An
alyses of Graph Algorithms\n\nThe number one criticism of average-case ana
lysis is that we do not actually know the probability distribution of real
-world inputs. Thus\, analyzing an algorithm on some random model has no i
mplications for practical performance. At its core\, this criticism doubts
the existence of external validity\, i.e.\, it assumes that algorithmic b
ehavior on the somewhat simple and clean models does not translate beyond
the models to practical performance real-world input. With this paper\, we
provide a first step towards studying the question of external validity s
ystematically. To this end\, we evaluate the performance of six graph algo
rithms on a collection of 2745 sparse real-world networks depending on two
properties\; the heterogeneity (variance in the degree distribution) and
locality (tendency of edges to connect vertices that are already close). W
e compare this with the performance on generated networks with varying loc
ality and heterogeneity. We find that the performance in the idealized set
ting of network models translates surprisingly well to real-world networks
. Moreover\, heterogeneity and locality appear to be the core properties i
mpacting the performance of many graph algorithms.\n
LOCATION:room Salle Emmy Noether
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Titouan Carette / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20230309T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20230309T113000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.424833966897
DESCRIPTION:Titouan Carette: Perfect matchings\, quantum computing and mon
oidal categories\n\nIn 2002\, Leslie Valiant designed a computational mode
l based on counting the number of perfect matchings of weighted graphs: th
e matchgates. Matchgates can directly be interpreted as quantum processes
providing an original combinatorial approach to quantum computing. In the
general case\, counting perfect matchings is #P-complete. However\, in the
specific case of planar graphs\, the FKT-algorithm allows counting perfec
t matchings in polynomial time. As a consequence\, planar matchgates provi
de a class of quantum computation that can be classically simulated in pol
ynomial time.Completely independently\, in 2010\, as a part of the categor
ical quantum mechanics program\, Coecke and Kissinger introduced the ZW-ca
lculus\, a graphical language inspired by two kinds of entanglement\, the
GHZ-states and W-states. This calculus quickly demonstrated interesting al
gebraic properties allowing it to be the first graphical language to be pr
oven universal and complete for all linear maps. In this talk\, I will pre
sent joint works with Étienne Moutot\, Thomas Perez and Renaud Vilmart\,
building a bridge between the two formalisms: matchgates and ZW-calculus.
It appears that reformulating matchgate theory into the category-theoretic
framework of ZW-calculus allows for a much simpler presentation. Converse
ly\, the matchgate approach provides the ZW-calculus with a straightforwar
d combinatorial interpretation. I will introduce a fragment of ZW-calculus
\, the planar W-calculus\, and show that it is universal and complete for
matchgates. Then I will present a variety of consequences\, from new algor
ithms for perfect matching counting and quantum simulation to a diagrammat
ical approach to determinant theory.\n
LOCATION:room Salle Grace Hopper
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ambroise Lafont / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20230109T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20230109T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.292425334229
DESCRIPTION:Ambroise Lafont: Generic pattern unification: a categorical ap
proach\n\nWe provide a generic categorical setting for Miller's pattern un
ification. The syntax with metavariables is generated by a free monad appl
ied to finite coproducts of representable functors\; the most general unif
ier is computed as a coequaliser in the associated multisorted Lawvere the
ory. Our setting handles simply-typed second-order syntax\, linear syntax\
, or (intrinsic) polymorphic syntax such as system F.\n
LOCATION:https://bbb.inria.fr/omi-t4o-kyz-won
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Duri Andrea Janett / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20230105T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20230105T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.854840955088
DESCRIPTION:Duri Andrea Janett: Two-Dimensional Drift Analysis: Optimizing
Two Functions Simultaneously Can Be Hard\n\nThe performance of Evolutiona
ry Algorithms (EAs) in dynamic environments\, that is\, environments in wh
ich the fitness function changes over time\, has recently been studied (e.
g.\, [Lengler\, Meier\, 2020]). In this talk\, we develop and analyse a mi
nimal example TwoLinear of a dynamic environment that can be hard for EAs.
The environment consists of two linear functions f1 and f2 with positive
weights 1 and n\, and in each generation selection is based on one of them
at random. They only differ in the set of positions that have weight 1 an
d n. We show that the (1+1)-EA with mutation rate χ/n is efficient for sm
all χ on TwoLinear\, but does not find the shared optimum in polynomial t
ime for large χ.To obtain the above result\, we apply drift analysis in t
wo dimensions. Drift analysis is one of the most powerful techniques to an
alyse the performance and behaviour of EAs. Previously\, it has only been
applied in one dimension. Here\, we are in the case of two random variable
s X1\, X2\, and the drift is approximatively given by A·(X1\, X2)T for a
matrix A. More precisely\, we are in the case where X1 and X2 impede each
other’s progress\, and we give a full characterisation of this case.\n
LOCATION:room Salle Philippe Flajolet
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dale Miller / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20221205T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20221205T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.852995798621
DESCRIPTION:Dale Miller: A positive perspective on term representation\n\n
Structural proof theory provides principles for organizing syntax. Many re
searchers have used the theory of proofs developed by Gentzen and Prawitz
to design both the representation of and operations on terms. In this talk
\, we illustrate this tight connection between proofs and terms by using t
he structure of proofs in the focused proof system LJF to design term stru
ctures. Since the proof theory of LJF does not determine a canonical polar
ization for primitive types\, two different approaches to term representat
ion arise. When primitive types are given the negative polarity\, LJF proo
fs encode terms as tree-like structures in a familiar fashion. In this sit
uation\, cut elimination also yields the familiar notion of substitution.
On the other hand\, when primitive types are given positive polarity\, LJF
proofs yield a structure in which explicit sharing of term structures is
possible. Such a representation of terms provides an explicit method for s
haring term structures. In this setting\, cut elimination yields a differe
nt notion of substitution. We illustrate these two approaches to term rep
resentation by applying them to encoding untyped lambda-terms. We also exp
loit concurrency theory techniques---traces and simulation---to compare un
typed lambda-terms using different structuring disciplines. [This is join
t work with Jui-Hsuan Wu and is based on a paper that will appear in CSL 2
023.]\n
LOCATION:https://bbb.inria.fr/omi-t4o-kyz-won
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Beniamino Accattoli / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20221128T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20221128T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.262499746366
DESCRIPTION:Beniamino Accattoli: Reasonable Space and the Lambda Calculus\
n\nThe lambda calculus is an expressive mathematical formalism that elegan
tly captures the core of functional programming languages. The evaluation
of programs is modeled as a symbolic rewriting system far from low-level i
mplementative details. This aspect has the drawback that it is not clear h
ow to measure the time and space complexity of functional programs in a re
asonable way\, that is\, in a way that agrees with standard computational
complexity. The talk focuses on reasonable space for the lambda calculus\,
about which---until very recently---almost nothing was known. The talk sh
all survey recent results in collaboration with Ugo Dal Lago and Gabriele
Vanoni (appeared in POPL 2021\, LICS 2021\, LICS 2022\, and ICFP 2022) whi
ch have clarified the topic\, and led to the first reasonable space cost m
odel for the lambda calculus able to account for logarithmic space.\n
LOCATION:https://bbb.inria.fr/omi-t4o-kyz-won
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Mehrnoosh Sadrzadeh / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20221121T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20221121T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.67942864102
DESCRIPTION:Mehrnoosh Sadrzadeh: Copying and Movement\, in Substructural L
ogics\, for Natural Language Reasoning\n\nIn 1958 Lambek proposed the logi
c of a residuated monoid to reason about syntax of natural language. This
logic was amongst the first substructural logics. It did not have contract
ion or weakening\, properties that indeed were not necessary for fixed wor
d order languages. As a result of these\, Lambek's logic could not reason
about free word order languages\, e.g. as in Sanskrit and Latin\, and dis
course structure\, e.g. as in "John slept. He snored." In this talk\, I w
ill show how endowing the logic with controlled modalities solves the prob
lem. I will go through the syntax and semantics of the logic and establish
applications to natural language. This is joint work with Lachlan McPheat
\, Hadi Wazni and Ian Lo Kin.\n
LOCATION:https://bbb.inria.fr/omi-t4o-kyz-won
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Hsien-Kuei Hwang / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20221109T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20221109T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.402745684094
DESCRIPTION:Hsien-Kuei Hwang: Bell numbers in Matsunaga's and Arima's Genj
ikō combinatorics: Modern perspectives and local limit theorems\n\nWe exa
mine and clarify in detail the contributions of Yoshisuke Matsunaga (1694?
--1744) to the computation of Bell numbers in the eighteenth century (in t
he Edo period)\, providing modern perspectives to some unknown materials t
hat are by far the earliest in the history of Bell numbers. Later clarific
ation and developments by Yoriyuki Arima (1714--1783)\, and several new re
sults such as the asymptotic distributions (notably the corresponding loca
l limit theorems) of a few closely related sequences are also given.\n
LOCATION:room Grace Hopper
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Marianela Morales / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20221107T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20221107T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.843575762099
DESCRIPTION:Marianela Morales: Looking inside the modalities: subatomic pr
oof theory for modal logics\n\nThere are many different cut-elimination te
chniques in the deep inference literature\, exploiting different aspects o
f the proof systems they work on. A particular methodology does however st
and out for its generality: cut-elimination via splitting. Even though thi
s proof has to be redone for every proof system anew\, there is a certain
repeating pattern. In order to formalize this pattern and to obtain a gene
ral cut-elimination method that works for many proof systems at the same t
ime\, the method of subatomic proof theory has been developed. The basic i
dea is to treat atoms as binary connectives\, leading to a uniform shape o
f all inference rules.\nIn our work in progress we extend this idea to cla
ssical modal logics. This means that also the unary modalities are treated
like binary connectives. We show soundness and completeness of the subato
mic system\, and we show cut-elimination via splitting for the linear frag
ment of the system.\n
LOCATION:https://bbb.inria.fr/omi-t4o-kyz-won
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Farah Al Wardani / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20221024T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20221024T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.232129376859
DESCRIPTION:Farah Al Wardani: Distributing and trusting proof checking\n\n
When a proof-checking kernel completes the checking of a formal proof\, th
at kernel asserts that a specific formula follows from a collection of lem
mas within a given logic. We describe a framework in which such an asserti
on can be made globally so that any other proof assistant willing to trust
that kernel can use that assertion without rechecking (or even understand
ing) the formal proof associated with that assertion. In this framework\,
we propose to move beyond autarkic proof checkers—i.e.\, self-sufficient
provers that trust proofs only when they are checked by their kernel—to
an explicitly non-autarkic setting. This framework must\, of course\, exp
licitly track which agents (proof checkers and their operators) are being
trusted when a trusting proof checker makes its assertions. We describe ho
w we have integrated this framework into a particular theorem prover while
making minor changes to how the prover inputs and outputs text files. Thi
s framework has been implemented using off-the-shelf web-based technologie
s\, such as JSON\, IPFS\, IPLD\, and public key cryptography.\n
LOCATION:https://bbb.inria.fr/omi-t4o-kyz-won
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Guillaume Berger / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20221020T090000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20221020T100000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.937127978189
DESCRIPTION:Guillaume Berger: Verification of cyber-physical systems: a co
unterexample-guided approach\n\nWe study counterexample-guided methods to
compute stability and safety certificates for hybrid linear systems. Count
erexample-guided methods involve interactions between a learner that produ
ces candidate certificates and an oracle that verifies whether a given can
didate certificate is valid. We consider two templates of polyhedral certi
ficates: a fixed-complexity and an adaptive-complexity template. In the fi
xed-complexity template\, the number of linear pieces of the certificate i
s fixed\; while in the adaptive-complexity template\, the number of linear
pieces is updated during the learning process. For both approaches\, we d
iscuss the advantages and disadvantages\, and we provide algorithmic frame
works for the computation of a certificate. Finally\, we discuss current w
ork involving extensions to correct-by-design controller synthesis.Guillau
me Berger is a postdoctoral researcher in the Programming Language Verific
ation (PLV) lab at CU Boulder\, in the team of Sriram Sankaranarayanan. He
received his PhD. in Mathematical Engineering from UCLouvain\, Belgium\,
in 2021. His research focuses on automatic techniques for verification and
design of complex modern systems\, like cyber-physical systems\, networke
d systems and hybrid systems.\n
LOCATION:room Henri Poincaré
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Riccardo Gozzi / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20221019T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20221019T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.961574289
DESCRIPTION:Riccardo Gozzi: Totalization of Ordinary Differential Equation
s\n\n"The totalization process was introduced by Denjoy in 1912 as an inte
rative procedure to obtain the antiderivative of any derivative. This idea
has generated the notion of Denjoy integral\, first of a serie of notions
of integration proposed in literature as alternatives to Riemann and Lebe
sgue integrals in order to successfully retrieve the antiderivative of som
e class of pathological derivatives. This talk follows the path taken by D
enjoy\, describing the details of its solution for the problem of integrat
ion\, and applies it to the realm of first order ODEs\, exploring the set
theoretical complexity of obtaining the solution of the dynamical system f
or ODEs with specific pathological right-hand terms."\n
LOCATION:room Grace Hopper
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Max S. New / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20221017T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20221017T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.0957876443736
DESCRIPTION:Max S. New: A type theory for formal category theory\n\nWe pre
sent a type theory for constructions and proofs in category theory. The ty
pe theory axiomatizes notions of category\, functor\, profunctor and a gen
eralized form of natural transformations. By restricting the type theory t
o an ordered linear variant of predicate logic\, we guarantee that all fun
ctions between categories are functorial\, all relations are profunctorial
\, and all transformations are natural by construction\, with no separate
proof necessary. Important category theoretic proofs such as the Yoneda le
mma become simple type theoretic proofs about the relationship between uni
t\, tensor and function types\, and can be seen to be ordered refinements
of familiar theorems in predicate logic. The type theory comes with a soun
d and complete notion of categorical model based on virtual equipments\, a
known setting for formal category theory that has been shown to model int
ernal\, enriched and indexed category theory. This means that while the pr
oofs in our type theory look like standard set-based arguments\, the synta
ctic discipline ensures that all proofs and constructions carry over to th
ese generalized settings as well.\n
LOCATION:https://us02web.zoom.us/j/89155612228?pwd=aU5RYXAvYXpvbmFROG44OVp
UVkxSZz09
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Martin Krejca / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20221013T113000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20221013T123000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.193835637215
DESCRIPTION:Martin Krejca: Accelerated Information Dissemination on Networ
ks with Local and Global Edges\n\n"Bootstrap percolation is a classical mo
del for the spread of information in a network. In the round-based version
\, nodes of an undirected graph become active once at least r neighbors we
re active in the previous round. We consider a slightly modified variant\,
acting on graphs that contain two types of edges—modeling local and glo
bal interactions\, respectively. In this model\, information spreads immed
iately via local edges but still requires a certain number r of active nei
ghbors in order to spread via global edges. We show for certain graph clas
ses that this modified process\, when starting with a single active node\,
results in a phase transition with respect to how quickly further nodes a
re activated. Initially\, the spread is rather slow\, but it gains signifi
cant speed once global edges are being used to activate nodes."\n
LOCATION:room Nicolaas Govert de Bruijn
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Simon Wietheger / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20221007T113000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20221007T123000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.527228416573
DESCRIPTION:Simon Wietheger: Crossover for Cardinality-Constrained Optimiz
ation\n\n"In order to understand better how and why crossover can benefit
optimization\, we consider pseudo-Boolean functions with an upper bound
𝐵 on the number of 1s allowed in the bit string (cardinality constraint
). We consider the natural translation of the OneMax test function\, a lin
ear function where 𝐵 bits have a weight of 1 + 𝜀 and the remaining b
its have a weight of 1. The literature gives a bound of Θ(𝑛^2) for the
(1+1) EA on this function. Part of the difficulty when optimizing this pr
oblem lies in having to improve individuals meeting the cardinality constr
aint by flipping both a 1 and a 0. The experimental literature proposes ba
lanced operators\, preserving the number of 1s\, as a remedy. We show that
a balanced mutation operator optimizes the problem in 𝑂 (𝑛 log 𝑛
) if\,𝑛 − 𝐵 = 𝑂 (1). However\, if 𝑛 − 𝐵 = Θ(𝑛)\, we
show a bound of Ω(𝑛^2)\, just as classic bit flip mutation. Crossover
and a simple island model gives 𝑂 (𝑛^2/log 𝑛) (uniform crossover
) and 𝑂 (𝑛√𝑛) (3-ary majority vote crossover). For balanced uni
form crossover with Hamming distance maximization for diversity we show a
bound of 𝑂 (𝑛 log 𝑛)."\n
LOCATION:room Poincaré
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Giti Omidvar / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20220905T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20220905T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.247045911219
DESCRIPTION:Giti Omidvar: Combinatorial Flows as Bicolored Atomic Flows\n\
nWe introduce a new graphical representation of proofs which we call combi
natorial flows. They can be seen as a generalization of atomic flows on on
e side and of combinatorial proofs on the other side. They inherit the clo
se correspondence with open deduction and the possibility of tracing atom
occurrences from atomic flows\, introduced by Guglielmi and Gundersen. The
correctness criterion\, on the other hand\, is inherited from combinatori
al proofs\, introduced by Hughes. Hence\, combinatorial flows form a proof
system in the sense of Cook and Rackhow. In this talk\, I will show how t
o translate an open deduction derivation to a combinatorial flow. Moreover
\, I will introduce a normalization process for combinatorial flows with u
nits.\n
LOCATION:https://us02web.zoom.us/j/89155612228?pwd=aU5RYXAvYXpvbmFROG44OVp
UVkxSZz09
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jui-Hsuan Wu (Ray) / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20220627T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20220627T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.57898531988
DESCRIPTION:Jui-Hsuan Wu (Ray): A positive perspective on term representat
ion\n\nThe structure of terms and expressions are represented variously vi
a\, say\, labeled trees or directed acyclic graphs (DAGs). When such expre
ssions contain bindings\, additional devices are needed. In this talk\, I
will present the focused proof system LJF as a framework for describing te
rm structures and substitution. Since the proof theory of LJF does not pic
k a canonical polarization for primitive types\, two different approaches
to term representation arise. When primitive types are given the negative
bias\, LJF proofs encode term structures as tree-like structures in a fami
liar fashion. In this situation\, cut elimination also yields the familiar
notion of substitution. On the other hand\, when primitive types are give
n the positive bias\, LJF proofs yield a structure in which explicit shari
ng of term structures is possible. In this situation\, cut elimination yie
lds a different notion of substitution. To illustrate these two approaches
to term representation\, I will give an example by applying them to the e
ncoding of untyped λ-terms.\n
LOCATION:https://us02web.zoom.us/j/89155612228?pwd=aU5RYXAvYXpvbmFROG44OVp
UVkxSZz09
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Riccardo Gozzi / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20220621T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20220621T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.78604724366
DESCRIPTION:Riccardo Gozzi: Analog characterization of complexity classee\
n\nIn the first part of the presentation I will introduce the concept of a
nalog computation in relation with integrator devices used in the 1940’s
to compute simple operations\, called differntial analyzers. A descriptio
n of the theoretical model behind the behaviors of those machine was first
provided by Shannon\, with his GPAC model which stands for Generable Purp
ose Analog Computation model. I will describe some of the main modificatio
ns that have been later applied in litterature to the model in order to si
mplify its formulation and improve its computational power. Following this
guideline\, I will then explain how these modifications led to an equival
ence between this model and the setting of computable analysis\, meaning t
hat every function that can be computed within the computable analysis fra
mework can also be computed by the GPAC model\, and viceversa. During the
course of this first\, introductory\, part of the talk\, the motivations a
t the core of this research will be discussed as well. In the second part
of the presentation I will illustrate how\, with the correct improvements
to the notion of computation of the GPAC model\, this particular equivalen
ce can be extended to the case of polynomial time complexity\, leading to
an equivalence between the well known complexity calss P and a certain cla
ss of systems of ODEs. To obtain this result it is required a way to encod
e and reproduce the behavior of the transiction function of a Turing machi
ne in a continuous setting\, keeping bounded the error introduced during t
his simulation.This second part of the talk will be more quantitative than
the first\, including more technical details. Finally\, in the last part
of the presentation\, I will briefly mention how the results previuosly sh
owed can be applied to further characterize higher complexity classes\, su
ch as EXPTIME or PSPACE\, with similar dynamical system.\n
LOCATION:room Grace Hopper
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Zhongdi QU / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20220621T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20220621T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.0445125792463
DESCRIPTION:Zhongdi QU: A First Runtime Analysis of the NSGA-II on a Multi
modal Problem\n\nVery recently\, the first mathematical runtime analyses o
f the multi-objective evolutionary optimizer NSGA-II have been conducted (
AAAI 2022\, GECCO 2022 (to appear)\, arxiv 2022). We continue this line of
research with a first runtime analysis of this algorithm on a benchmark p
roblem consisting of two multimodal objectives. We prove that if the popul
ation size $N$ is at least four times the size of the Pareto front\, then
the NSGA-II with four different ways to select parents and bit-wise mutati
on optimizes the OneJumpZeroJump benchmark with jump size $2 \\le k \\le n
/4$ in time $O(N n^k)$. When using fast mutation\, a recently proposed hea
vy-tailed mutation operator\, this guarantee improves by a factor of $k^{\
\Omega(k)}$. Overall\, this work shows that the NSGA-II copes with the loc
al optima of the OneJumpZeroJump problem at least as well as the global SE
MO algorithm.\n
LOCATION:room Philippe Flajolet
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Bryce Clarke / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20220620T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20220620T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.293989854797
DESCRIPTION:Bryce Clarke: Investigating lenses between preordered sets\n\n
Bidirectional transformations are a means of maintaining consistency betwe
en a pair of systems. In 2005\, the mathematical structure of a lens was i
ntroduced to model bidirectional transformations\, and has since grown int
o an active topic of research in computer science and applied category the
ory. Classically\, a system may be modelled by its set of possible states\
, leading to a particular notion of lens\, however as more sophisticated m
odels of systems have developed\, more interesting and useful notions of l
ens have arisen.\n\nThe aim of this talk is to investigate lenses between
preordered sets. The principal idea is that a system is modelled by its se
t of states equipped with a preorder\, which specifies when one state may
transition to another\, while a lens is an order-preserving function with
certain additional structure. Throughout the talk we will explore answers
to several natural questions regarding the mathematical structure of lense
s. How do lenses compose and decompose\, both sequentially and in parallel
? What are the ways in which we can build new lenses with nice properties?
Given an order-preserving function\, how many lens structures does it adm
it\, and is it possible to freely generate a lens structure from it? The t
alk will focus on demonstrating answers to these questions via small "toy"
examples\, and aims to be accessible without prior knowledge of category
theory. If time allows\, I will discuss how the framework of lenses may be
extended when systems are instead modelled by generalised metric spaces o
r weighted categories.\n
LOCATION:https://us02web.zoom.us/j/89155612228?pwd=aU5RYXAvYXpvbmFROG44OVp
UVkxSZz09
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Pablo Donato / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20220530T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20220530T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.199261419431
DESCRIPTION:Pablo Donato: Interactive Deep Reasoning\n\nIn this talk\, I w
ill present the work I have been doing for my thesis in the past year and
a half\, which is an exploration in how to build formal proofs interactive
ly through graphical\, deep inference proof systems.\n\nI will start with
a demonstration of Actema\, a prototype of graphical user interface for th
eorem proving in intuitionistic FOL based on direct manipulation of the pr
oof state. A notable feature is the ability to reason by drag-and-dropping
formulas within a sequent\, which is a direct application of the subformu
la linking paradigm of K. Chaudhuri. The specificity of our approach lies
in how we handle quantifiers through unification\, as well as equalities.
This enables both an elegant characterization\, and a wide generalization
of the behavior of standard rewrite tactics.\n\nIn the second part\, I wil
l present the "Bubble Calculus"\, a new kind of nested sequent system whic
h comes equipped with a nice graphical syntax. Inspired by the membranes o
f the Chemical Abstract Machine of Boudol and Berry\, we add a so-called "
bubble" construct for localizing interactions between propositions\, which
can be understood as internalizing the notion of premiss/subgoal inside j
udgments. By allowing bubbles to be polarized\, one can then recover intui
tionistic\, dual-intuitionistic\, bi-intuitionistic and classical logic as
fragments which differ only in the allowed switch/membrane traversal rule
s.\n\nIn the third and last part\, I will introduce an intuitionistic vari
ant of the existential graphs of C. S. Peirce\, arguably the first graphic
al proof system in the western logic tradition. To make the notation more
readable\, I will use a botanical metaphor where the graphs are represente
d as (nested) flowers. Contrarily to bubbles\, flowers have a linear trans
lation to and from traditional formulas\, which allows to get completely r
id of the latter in the proof system.\n
LOCATION:https://us02web.zoom.us/j/89155612228?pwd=aU5RYXAvYXpvbmFROG44OVp
UVkxSZz09
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Willem Heijltjes / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20220523T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20220523T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.285535241052
DESCRIPTION:Willem Heijltjes: The Functional Machine Calculus\n\nI will pr
esent the Functional Machine Calculus (FMC)\, a simple model of higher-ord
er computation with "reader/writer" effects: state\, input/output\, probab
ilities\, and non-determinism. The main result is to extend two fundamenta
l properties of the lambda-calculus to these effects: reduction in the FMC
is confluent\, and a system of simple types confers strong normalization.
\n\nThe premise is to view the lambda-calculus as an instruction language
for a simple stack machine\, in the standard way of the Krivine machine\,
where application is "push" and abstraction is "pop". The FMC then consist
s of two independent generalizations\, that are natural from the perspecti
ve of the machine.\n\nThe first generalization\, "locations"\, is to allow
multiple stacks (or streams) on the machine\, each indicated by a "locati
on". Application and abstraction are parameterized in these locations\, to
give push and pop actions on the relevant stack. Then input streams\, out
put streams\, and memory cells are straightforwardly modelled by distinct
locations.\n\nThe second generalization\, "sequencing"\, introduces sequen
tial composition\, following the perspective of terms as sequences of mach
ine instructions\, as well as a unit\, the empty sequence. This is known f
rom Hasegawa's kappa-calculus and from concatenative programming languages
\, and enables the encoding of reduction strategies\, including call-by-va
lue lambda-calculus\, and for the given effects\, Moggi's metalanguage\, L
evy's call-by-push-value\, and Haskell Arrows.\n\nReduction in the FMC is
confluent\, which is possible because encoded effect operations reduce alg
ebraically\, rather than operationally. It can be simply typed to confer s
trong normalization\, and because effectful operations are fully typed\, i
t has a semantics as a Cartesian closed category. Unlike in the monadic se
tting\, reader/writer effects in the FMC combine seemlessly.\n
LOCATION:https://webconf.math.cnrs.fr/b/noa-p22-a7m
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Joël Ouaknine / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20220519T143000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20220519T153000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.493667348655
DESCRIPTION:Joël Ouaknine: The Skolem Landscape\n\nThe Skolem Problem ask
s how to determine algorithmically whether a given linear recurrence seque
nce (such as the Fibonacci numbers) has a zero. It is a central question i
n dynamical systems and number theory\, and has many connections to other
branches of mathematics and computer science. Unfortunately\, its decidabi
lity has been open for nearly a century! In this talk\, I will present a s
urvey of what is known on the Skolem Problem and related questions\, inclu
ding recent and ongoing developments.\n
LOCATION:room Sophie Germain + online upon request
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dylan McDermott / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20220509T153000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20220509T163000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.92776139713
DESCRIPTION:Dylan McDermott: Higher-order algebraic theories\n\nFirst-orde
r algebraic theories describe algebraic structures that can be presented b
y a collection of operators and equations. These were generalized by Fiore
et al. to second-order algebraic theories\, in which the operators can bi
nd simple variables. Examples include lambda-abstraction in the untyped la
mbda-calculus\, and quantification in first-order logic.\n\nWe generalize
to higher-order theories\, in which operators can bind variables of higher
orders. I will discuss the resulting notion of nth-order algebraic theory
\, and some examples. Nth-order theories have a rich metatheory\, in parti
cular they have a universal characterization as a completion\, under a cla
ss of colimits\, of a freely generated category. It follows from this that
there is a correspondence between (n+1)th-order algebraic theories and ce
rtain monads on nth-order algebraic theories\, analogous to the correspond
ence between (monosorted) first-order theories and finitary monads on Set.
\n\nThis is joint work with Nathanael Arkor.\n
LOCATION:https://webconf.math.cnrs.fr/b/noa-p22-a7m
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Franck Djeumou / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20220414T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20220414T160000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.760613491376
DESCRIPTION:Franck Djeumou: Neural Networks with Physics-Informed Architec
tures and Constraints for Dynamical Systems Modeling\n\nEffective inclusio
n of physics-based knowledge into deep neural network models of dynamical
systems can greatly improve data efficiency and generalization. Such a pri
ori knowledge might arise from physical principles (e.g.\, conservation la
ws) or from the system's design (e.g.\, the Jacobian matrix of a robot)\,
even if large portions of the system dynamics remain unknown. We develop a
framework to learn dynamics models from trajectory data while incorporati
ng a priori system knowledge as inductive bias. By exploiting a priori sys
tem knowledge during training\, the proposed approach learns to predict th
e system dynamics two orders of magnitude more accurately than a baseline
approach that does not include prior knowledge\, given the same training d
ataset.\n
LOCATION:https://ecolepolytechnique.zoom.us/j/87240940887 (online\, live f
rom Austin\, Texas\, US)
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Elena Ivanova / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20220406T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20220406T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.651720883313
DESCRIPTION:Elena Ivanova: Efficient Synthesis of Controllers using Abstra
ction-Based Approaches\n\nThe first part of the talk will be dedicated to
a control synthesis for cyber-physical systems using abstraction-based con
trol synthesis approaches. These approaches first create a finite-state ab
straction (or a symbolic model) for a continuous or hybrid system and then
refine the controller synthesized for the abstraction to a controller for
the original system. Abstraction-based control synthesis techniques allow
us to handle complex dynamics of CPS models and non-trivial specification
s (for instance given by LTL formulas) but suffer from poor scalability. I
will talk about how to improve the efficiency of ABS approaches when safe
ty specification is considered. The second part of the talk will be dedica
ted to ongoing research on efficient approximations of the reachable sets.
\n
LOCATION:room Grace Hopper
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Léo Paviet Salomon / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20220324T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20220324T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.699730387233
DESCRIPTION:Léo Paviet Salomon: Groupe fondamental et pavages du plan: qu
elques constructions\n\nOn appelle sous-shift (ou sous-décalage) un ensem
ble de pavages ou de coloriages du plan respectant certaines contraintes l
ocales. Historiquement introduits comme discrétisations de systèmes dyna
miques continus\, on se propose ici d'en étudier un invariant topologique
\, introduit par W.Geller et J.Propp\, le Groupe Fondamental Projectif. A
l'instar de la définition habituelle du groupe fondamental\, un invariant
d'espaces topologiques\, il s'agira ici de comprendre comment l'on peut d
éfinir une notion de chemins dans les pavages\, reliant les configuration
s entre elles\, et d'étudier comment les déformations de ces chemins per
mettent d'associer à chaque pavage un unique objet algébrique: son group
e fondamental projectif. En particulier\, on montrera dans cet exposé com
ment réaliser une large classe de groupes comme groupes fondamentaux de c
ertains pavages.\n
LOCATION:room Salle Henri Poincaré
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nathan Grosshans / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20220317T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20220317T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.198660299355
DESCRIPTION:Nathan Grosshans: Visibly pushdown languages in AC⁰\n\nOne i
mportant research endeavour at the intersection of circuit complexity theo
ry\, algebraic automata\ntheory and logic is the classification of regular
languages according to their localisation\nwithin the internal structure
of NC¹\, the class of languages decided by Boolean circuits of polynomial
size\, logarithmic depth and with gates of constant fan-in. In some sense
\, the search for such a classification concentrates most of the open ques
tions we have about the relationship between NC1 and its well-studied subc
lasses.\n\nWhile many questions are still open\, one of the greatest succe
sses of this research endeavour has been the characterisation of the regul
ar languages in AC⁰\, the subclass of NC¹ corresponding to Boolean cir
cuits of polynomial length\, constant depth and with gates of unbounded fa
n-in. This characterisation takes the form of a triple languages-algebra-l
ogic correspondence: a regular language is in AC0 if and only if its synta
ctic morphism is quasi-aperiodic if and only if it is definable in first-o
rder logic over words with linear order and modular predicates.\n\nIt is n
atural to try to extend such results to classes of formal languages great
er than the class of regular languages. A well studied and robust such cl
ass is given by visibly pushdown languages (VPLs): languages recognised by
pushdown automata where the stack-height-behaviour only depends on the l
etters read from the input. Over the previous decade\, a series of works
concentrated on the fine complexity of VPLs\, with several achievements:
one of those was a characterisation of the class of visibly counter langu
ages (basically VPLs recognised by visibly pushdown automata with only on
e stack symbol) in AC⁰ by Krebs\, Lange and Ludwig. However\, the chara
cterisation of the VPLs in AC⁰ still remains open.\n\nIn this talk\, I
shall present a conjectural characterisation of the VPLs in AC⁰ obtained
with Stefan Göller at the Universität Kassel. It is inspired by the con
jectural characterisation given by Ludwig in his Ph.D. thesis as a genera
lisation of the characterisation for visibly counter languages\, but that
is actually false. In fact\, we give a more precise general conjectural c
haracterisation that builds upon recognisability by morphisms into Ext-alg
ebras\, an extension of recognisability by monoid-morphisms proposed by C
zarnetzki\, Krebs and Lange to suit the case of VPLs. This characterisatio
n classifies the VPLs into three categories according to precise condition
s on the Ext-algebra-morphisms that recognise them:\n- those that are TC
⁰-hard\;\n- those that are in AC⁰\;\n- those that correspond to a well
-identified class of "intermediate languages" that we believe to be neithe
r in AC⁰ nor TC⁰-hard.\n
LOCATION:https://ecolepolytechnique.zoom.us/j/87240940887 (online)
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Paolo Pistone / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20220307T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20220307T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.470028790811
DESCRIPTION:Paolo Pistone: On Equivalence and Similarity of Polymorphic Pr
oofs and Programs\n\nUnder the proofs-as-programs paradigm\, the problem o
f program equivalence\, that is\, of understanding whether two programs co
mpute the same function\, can be related to the problem of equivalence pro
of\, that is\, of understanding whether two formal derivations represent\,
in some sense\, the same proof. In this talk I will discuss some methods
to capture program/proof equivalence in System F\, the paradigmatic langua
ge for parametric polymorphism\, through the definition of an invariant\,
for each type\, called the characteristic. This invariant provides a means
to know whether\, in the proofs of a given formula\, propositional quanti
fication (i.e. polymorphism) is eliminable via parametricity\, yielding a
way to test equivalence in a finite way. Moreover\, I will sketch how para
metricity and related methods for equivalence can be lifted to a more quan
titative setting (as those arising from probabilistic or approximate compu
tation) in which the vital property to understand is whether two programs\
, albeit non-equivalent\, behave in a sufficiently similar way\, so that r
eplacing the one by the other cannot alter the results of computation too
much.\n
LOCATION:https://webconf.math.cnrs.fr/b/noa-p22-a7m
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Martin Krejca / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20220217T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20220217T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.14948884375
DESCRIPTION:Martin Krejca: The Power of Probabilistic Models in Optimizati
on\n\nFor many real-world optimization problems\, the objective function i
s only indirectly accessible\, for example\, via simulations. In this sett
ing\, randomized search heuristics (RSHs) are applied to great success\, g
uided solely by the quality of samples. One important class of these heuri
stics are estimation-of-distribution algorithms (EDAs)\, which maintain an
d refine a probabilistic model of the search space.\n\nIn this talk\, I di
scuss some of my results on the theoretical analysis of EDAs by presenting
properties of EDAs that set them apart from other RSHs. We see that EDAs
cope inherently well with noisy objective functions\, due to the probabili
stic model tolerating faulty updates to a certain degree. However\, we als
o show that these models typically degenerate if important updates are wit
hheld for longer periods of time. We conclude by presenting how this probl
em is circumvented when applying better rules to handle updates.\n
LOCATION:room Salle Philippe Flajolet
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ulysse Chabaud / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20220203T163000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20220203T173000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.529643409159
DESCRIPTION:Ulysse Chabaud: Holomorphic Quantum Computing\n\nThe advent of
quantum information processing promises dramatic advantages with respect
to its classical counterpart\, notably for computing. I will give an intro
duction to quantum computing through the lens of holomorphic functions\, w
hich allow us to elegantly describe both discrete- and continuous-variable
quantum computations\, using classical dynamical systems. As an applicati
on\, I will discuss the characterisation of quantum properties that are ne
cessary resources for quantum computational advantages\, such as non-Gauss
ianity or entanglement.\n\nJoint work with Saeed Merhaban ([arXiv:2111.001
17](https://arxiv.org/abs/2111.00117)).\n
LOCATION:https://ecolepolytechnique.zoom.us/j/87240940887 (online\, live f
rom California)
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ambroise Lafont / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20211025T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20211025T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.94420595785
DESCRIPTION:Ambroise Lafont: Variable binding and substitution for (namele
ss) dummies\n\n[Organizer's note: this will be a hybrid seminar\, simultan
eously taking place\nat Salle Marcel-Paul Schützenberger and [on BBB](htt
ps://webconf.math.cnrs.fr/b/noa-p22-a7m).]\n\nBy abstracting over well-kno
wn properties of De Bruijn's\nrepresentation with nameless dummies\, we de
sign a new theory of syntax\nwith variable binding and capture-avoiding su
bstitution. We propose\nit as a simpler alternative to Fiore\, Plotkin\,
and Turi's approach\,\nwith which we establish a strong formal link. We al
so show that our\ntheory easily incorporates simple types and equations be
tween terms.\n\nJoint work with Tom & Andre Hirschowitz\, Marco Maggesi\n
LOCATION:room Marcel-Paul Schützenberger
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tarmo Uustalu / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20211018T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20211018T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.0388392681782
DESCRIPTION:Tarmo Uustalu: List monads\n\nWe tend to speak of the (possibl
y empty) list monad and the\nnonempty list monad\, meaning the free monoid
monad and the free\nsemigroup monad\, as if those were the only monad str
uctures on the\nlist and nonempty list endofunctors (on Set). But they are
not! It\nmay at first seem hard to construct other list and nonempty list
\nmonads\, but at a closer look it turns out that examples\nabound. There
are infinitely many list monads with the singleton\nfunction as the unit t
hat admit a presentation with one nullary\nand one binary operation\, and
infinitely many nonempty list monads\nwith singleton as the unit and a pre
sentation with one binary\noperation\; some multiplications not only delet
e\, but even\nduplicate and permute elements. There are list and nonempty
list\nmonads with singleton as the unit that have no finite\npresentation.
There are nonempty list monads whose unit is the\ndoubleton function. Y
ou cannot tell if a nonempty list monad\npresented to you as a blackbox is
the free semigroup monad by\ntesting the unit and multiplication on finit
ely many\ninputs. Etc. We are far from having classified all list monads o
r\nall nonempty list monads\, but these are cool combinatorial\nproblems.\
n\nThis is joint work with Dylan McDermott and Maciej Piróg.\n
LOCATION:https://webconf.math.cnrs.fr/b/noa-p22-a7m
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Constantin Enea / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20211005T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20211005T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.384082515531
DESCRIPTION:Constantin Enea: Towards Automated Verification of Concurrent
or Distributed Software\n\nI will talk about recent results concerning the
problem of increasing the level of automation in formal verification of c
oncurrent or distributed programs. These results span various approaches f
rom testing\, finite state model-checking\, to SMT-based proofs. Also\, th
ey apply to various classes of programs from concurrent data types\, to di
stributed databases\, or applications thereof.\n
LOCATION:room Philippe Flajolet
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Christian Johansen / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210707T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210707T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.392109568233
DESCRIPTION:Christian Johansen: History-aware Higher Dimensional Modal Log
ic\n\nThis talk presents a modal logic over HDAs which incorporates two\nm
odalities for reasoning about “during” and “after”. This higher\nd
imensional modal logic (HDML) is decidable and an “almost” complete\na
xiomatic system exists for it. When the HDA model is restricted to\nKripk
e structures\, a syntactic restriction of HDML becomes the standard\nmodal
logic. One can isolate the class of HDAs that encode Mazurkiewicz\ntrace
s and show how HDML\, with natural definitions of corresponding\nUntil ope
rators\, can be restricted to LTrL (the linear time temporal\nlogic over M
azurkiewicz traces) or the branching time ISTL. A\npreliminary study of th
e expressiveness of the basic HDML language wrt.\nbisimulations has conclu
ded that HDML captures the split-bisimulation.\nOne can also add backward-
looking modalities (i.e.\, past modalities) so\nto increase the expressive
ness so to be able to capture the hereditary\nhistory-preserving bisimulat
ion. Classical examples from the literature\nthat are used to distinguish
one-or-another bisimulation can be\ndistinguished in this hHDML using a sp
ecially crafted formula. I will\nshow these interesting examples and talk
about the respective\nliterature\, if time permits.\n
LOCATION:https://webconf.math.cnrs.fr/b/sam-tq6-hwg
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sven Dziadek / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210630T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210630T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.253211172353
DESCRIPTION:Sven Dziadek: Greibach Normal Form and Simple Automata for Wei
ghted ω-Context-Free Languages\n\nIn weighted automata theory\, many clas
sical results on formal languages have been extended into a quantitative s
etting. Here\, we investigate weighted context-free languages of infinite
words\, a generalization of ω-context-free languages (Cohen\, Gold 1977)
and an extension of weighted context-free languages of finite words (Choms
ky\, Schützenberger 1963). As in the theory of formal grammars\, these we
ighted context-free languages\, or ω-algebraic series\, can be represente
d as solutions of (mixed) ω-algebraic systems of equations and by weighte
d ω-pushdown automata.\n\nIn our first main result\, we show that (mixed)
ω-algebraic systems can be transformed into Greibach normal form. We use
the Greibach normal form in our second main result to prove that simple
ω-reset pushdown automata recognize all ω-algebraic series. Simple ω-re
set automata do not use ε-transitions and can change the stack only by at
most one symbol. These results generalize fundamental properties of conte
xt-free languages to weighted context-free languages.\n\nThis talk is base
d on [this article](https://arxiv.org/abs/2007.08866) and its correspondin
g [short version](https://doi.org/10.4230/LIPIcs.FSTTCS.2019.38).\n
LOCATION:https://ecolepolytechnique.zoom.us/j/88289865159?pwd=SFlKRmFOcTM1
OUdqUkFBbnp6WFR6UT09
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sonia Vanier / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210624T143000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210624T153000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.283875169948
DESCRIPTION:Sonia Vanier: Distributed Denial of Service cyber-attacks in 5
G networks: a robust approximation approach\n\nDistributed Denial of Servi
ce (DDoS) cyberattacks represent a major security risk for network operato
rs and internet service providers. They thus need to invest in security so
lutions to protect their network against DDoS attacks. The present work fo
cuses on deploying a network function virtualization based architecture to
secure a network against an on-going DDoS attack. We assume that the targ
et\, sources and volume of the attack have been identified. However\, due
e.g. to 5G network slicing\, the exact routing of the illegitimate flow in
the network is not known by the internet service provider. We seek to det
ermine the optimal number and locations of virtual network functions in or
der to remove all the illegitimate traffic while minimizing the total cost
of the activated virtual network functions. We propose a robust optimizat
ion framework to solve this problem. The uncertain input parameters corres
pond to the amount of illegitimate flow on each path connecting an attack
source to the target and can take values within a predefined uncertainty s
et. In order to solve this robust optimization problem\, we develop an adv
ersarial approach in which the adversarial sub-problem is solved by a Bran
ch & Price algorithm. The results of our computational experiments\, carri
ed out on medium-size randomly generated instances\, show that the propose
d solution approach is able to provide optimal solutions within short comp
utation times\n
LOCATION:https://ecolepolytechnique.zoom.us/j/87240940887
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alex Kavvos / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210623T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210623T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.329789209985
DESCRIPTION:Alex Kavvos: Client-Server Sessions in Linear Logic\n\nWe intr
oduce coexponentials\, a new set of modalities for Classical Linear Logic.
As duals to exponentials\, the coexponentials codify a distributed form o
f the structural rules of weakening and contraction. This makes them a sui
table logical device for encapsulating the pattern of a server receiving r
equests from an arbitrary number of clients on a single channel. Guided by
this intuition we formulate a system of session types based on Classical
Linear Logic with coexponentials\, which is suited to modelling client-ser
ver interactions. We also present a session-typed functional programming l
anguage for client-server programming\, which we translate to our system o
f coexponentials.\n
LOCATION:https://webconf.math.cnrs.fr/b/noa-p22-a7m
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Krzysztof Ziemiański / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210623T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210623T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.577013655864
DESCRIPTION:Krzysztof Ziemiański: Tracks in Higher Dimensional Automata\n
\nThe main goal of my talk is to present two models of executions of Highe
r Dimensional Automata. A track in a HDA is a sequence of cells such that
every cell is either an upper face or an upper coface of the preceding one
. To every track we can assign the (evi)pomset of its events\; it is a lab
eled interval order equipped with an additional secondary ordering. Then w
e consider the set of tracks between fixed source and target cells\, up to
certain equivalence. This set is naturally a presheaf over the category o
f evipomsets\, which is our first model of executions of HDA. This model c
an be simplified. When we restrict to step-sequence executions\, ie\, trac
ks in which the consecutive cells have only one common vertex\, we obtain
a presheaf over permutahedral category. This model is combinatorially simp
ler. At first glance it seems too restrictive but there is some evidence t
hat this is not the case: the space of topological executions is homotopy
equivalent to the geometric realization of the permutahedral model.\n
LOCATION:https://webconf.math.cnrs.fr/b/sam-tq6-hwg
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Federico Olimpieri / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210607T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210607T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.449660589319
DESCRIPTION:Federico Olimpieri: Intersection type distributors\n\nWe study
a family of distributors-induced bicategorical models of\nlambda-calculus
\, proving that they can be syntactically presented\nvia intersection type
systems. We first introduce a class of\n2-monads whose algebras are monoi
dal categories modelling resource\nmanagement. We lift these monads to dis
tributors and define a\nparametric Kleisli bicategory\, giving a sufficien
t condition for\nits cartesian closure. In this framework we define a\npro
of-relevant semantics: the interpretation of a term associates\nto it the
set of its typing derivations in appropriate systems.\nWe prove that our m
odel characterize solvability\, adapting\nreducibility techniques to our s
etting. We conclude by describing\ntwo examples of our construction.\n
LOCATION:https://webconf.math.cnrs.fr/b/noa-p22-a7m
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Francesco Gavazzo / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210519T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210519T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.0369198917728
DESCRIPTION:Francesco Gavazzo: On Monadic Rewriting Systems\n\nMotivated b
y the study of effectful programming languages and computations\, I will i
ntroduce the theory of monadic rewriting systems. The latter are rewriting
systems whose notion of reduction is effectful\, effects being modelled a
s monads. Such systems are to effectful computations and programming langu
ages what traditional rewriting systems are to pure computations and progr
amming languages. Contrary to what happens in the ordinary operational sem
antics of monadic programming languages\, defining mathematically and oper
ationally meaningful notions of monadic rewriting turns out to be simply n
ot possible for several monads\, including the distribution\, powerset\, r
eader\, and global state monad. This raises the question of when monadic r
ewriting is possible.\n\nI will answer that question by showing that the s
o-called weakly cartesian monads precisely describe computational effects
for which monadic rewriting is well-behaved. If monads are given as equati
onal theories\, as it is in the case of algebraic effects\, a sufficient c
ondition ensuring monadic rewriting to be well-behaved can be given by loo
king at the shape of the theory only: such a condition dates back to an ol
d theory by Guatam and requires equations to be linear. Finally\, I will a
pply the abstract theory of monadic rewriting systems to the call-by-value
λ-calculus with algebraic effects\, this way obtaining the extension of
the well-known confluence and standardisation theorems to an effectful set
ting.\n
LOCATION:https://webconf.math.cnrs.fr/b/sam-tq6-hwg
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Riccardo Gozzi / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210512T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210512T113000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.519735620611
DESCRIPTION:Riccardo Gozzi: Analog characterization of standard complexity
classes by means of ODEs\n\nIn this presentation it will be shown how to
make use of ordinary differential equations (ODEs) to describe standard co
mplexity classes. Previously it was shown that the classes P and FP can be
characterized with ODEs. Here we show that ODEs can also be used to chara
cterize a wide range of computable functions\, from exponentials up to inc
luding all elementary functions. It will be also discussed the case of spa
ce complexity classes\, introducing the definition of a particular dynamic
al system able to describe functions in FPSPACE. Finally\, to complement
what have been done with functions\, the treatment of classes of languages
such as EXPTIME and PSPACE will be included in the analysis.\n
LOCATION:https://ecolepolytechnique.zoom.us/j/87240940887
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Georg Struth / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210421T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210421T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.652787515466
DESCRIPTION:Georg Struth: Verifying Hybrid Systems with Interactive Theore
m Provers\n\nHybrid systems integrate continuous dynamics and discrete\nco
ntrol. A prominent approach is differential dynamic logic (dL)\, a\nmodal
logic for reasoning about ordinary differential equations and\ntheir solut
ions within hybrid programs. Over the last decade\, a\ndomain-specific se
quent calculus for dL has been developed together\nwith an intricate expli
cit substitution calculus for it. It has been\nintegrated into the KeYmaer
a X tool and proved its worth in numerous\ncase studies.\n\nThis talk pres
ents an algebraic reconstruction of this approach and\nthe first verificat
ion and refinement components in an interactive\nproof assistant inspired
by it. Our components are based on shallow\nembeddings in which the proof
theory of dL is by and large replaced by\nsemantic equational reasoning ab
out orbits and trajectories of\ndynamical systems in combination with disc
rete state updates. We use\nalgebras\, in particular variants of Kleene a
lgebras and predicate\ntransformer algebras\, for automatic verification c
ondition\ngeneration. We currently support a component for reasoning with\
nweakest liberal preconditions\, a Hoare logic and a refinement calculus\n
for hybrid programs.\n\nThese allow us to verify hybrid programs in variou
s ways: starting\nfrom hybrid program specifications based on ordinary dif
ferential\nequations\, we can certify solutions of locally Lipschitz-conti
nuous\nvector fields using the Picard-Lindelöf theorem and then reason\ne
xplicitly about them. Alternatively we can represent solutions of\ncontinu
ous vector fields implicitly by invariant sets. Finally\, we can\nanalyse
hybrid program that specify trajectories or orbits of hybrid\nsystems dire
ctly.\n\nApart from presenting the algebras used and their extension and\n
instantiation to hybrid program semantics\, I will present some\nexamples\
, comment on the intricacies of formalising the approach\nwithin the Isabe
lle/HOL proof assistant\, and outline some future\ndirections for this lin
e of work\, time permitting.\n\nThis work is joint with Jonathan Julián H
uerta y Munive\, and partially\nfunded by CONACYT.\n
LOCATION:https://webconf.math.cnrs.fr/b/sam-tq6-hwg
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Renaud Vilmart / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210414T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210414T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.946491080547
DESCRIPTION:Renaud Vilmart: An introduction to ZX-calculus\n\nThe ZX-Calcu
lus is a powerful graphical language for representing quantum processes\,
stemming from category theory. Its primitives are close to that of the har
dware these processes will supposedly be implemented on\, and yet it enjoy
s some level of abstraction. In particular\, it is equipped with an intuit
ive equational theory\, allowing us to relate processes that are equivalen
t\, i.e. that represent the same quantum evolution. The plasticity and the
equational theory of the language make it a particularly good candidate f
or unifying different models of quantum computation\, for optimisation\, a
s well as for verifying properties or equivalences of processes.\n
LOCATION:https://webconf.math.cnrs.fr/b/sam-tq6-hwg
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Janna Burman / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210408T143000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210408T153000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.711333424949
DESCRIPTION:Janna Burman: Time-Optimal Self-Stabilizing Leader Election in
Population Protocols\n\nWe consider the standard population protocol mode
l\, where (a\npriori) indistinguishable and anonymous agents interact in p
airs\naccording to uniformly random scheduling. The self-stabilizing\nlead
er election problem requires the protocol to converge on a\nsingle leader
agent from any possible initial configuration. We\ninitiate the study of t
ime complexity of population protocols\nsolving this problem in its origin
al setting: with probability 1\,\nin a complete communication graph. The o
nly previously known\nprotocol by Cai\, Izumi\, and Wada [Theor. Comput. S
yst. 50] runs\nin expected parallel time Θ(n²) and has the optimal numbe
r\nof n states in a population of n agents. The existing protocol\nhas the
additional property that it becomes silent\, i.e.\, the\nagents' states e
ventually stop changing.\n\nObserving that any silent protocol solving sel
f-stabilizing leader election requires Ω(n) expected parallel time\, we i
ntroduce a silent protocol that uses optimal O(n) parallel time and states
. Without any silence constraints\, we show that it is possible to solve s
elf-stabilizing leader election in asymptotically optimal expected paralle
l time of O(log n)\, but using at least exponential states (a quasi-polyn
omial number of bits). All of our protocols (and also that of Cai et al.)
work by solving the more difficult ranking problem: assigning agents the r
anks 1\, … \,n.\n
LOCATION:https://ecolepolytechnique.zoom.us/j/82016424508
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Benoit Monin / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210401T143000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210401T153000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.283653266281
DESCRIPTION:Benoit Monin: Une petite histoire de la K-trivialité\n\nLa co
mplexité de Kolmogorov est utilisée avec succès pour\ncaractériser l'a
léatoire pour les chaînes binaires infinies : Il\ns'agit des chaînes do
nt la complexité de Kolmogorov de leurs\npréfixes est maximale. A l'oppo
sé\, les chaînes binaires infinies\ndites "K-triviales" sont celles dont
la complexité de Kolmogorov\nde leurs préfixes est minimale. La classe
des K-triviaux est\ndénombrable\, et contient "juste un peu plus" que les
chaînes\nbinaires infinies calculables. Les nombreuses études sur les\n
K-triviaux depuis une vingtaine d'années ont révélé la grande\nrichess
e de cette classe. Nous en présenterons les différents\naspects.\n
LOCATION:https://ecolepolytechnique.zoom.us/j/82016424508
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Arnaud Spiwack / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210331T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210331T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.40469264734
DESCRIPTION:Arnaud Spiwack: Linear Constraints\n\nIn the past few years\,
I've been involved in extending the type\nsystem of the Haskell programmin
g language to support linear\ntypes. In one sentence\, a linear argument m
ust be consumed\nexactly once in the body of its function\; a linear funct
ion is a\nfunction whose argument is linear. Such a linear type system\nco
mes from linear logic (or\, in this particular case\,\nintuitionistic line
ar logic\, but who's counting?) seen through\nthe lens of the Curry-Howard
correspondence. Linear typing has\ntwo main families of applications: mak
ing pure interface to\nmutable data structures\, such as arrays (“pure
” means that\nfunctions are functions in the sense of mathematics)\; and
\nenforcing protocol in the type level\, for instance making sure\nfile ha
ndles are eventually closed and not written to after being\nclosed. An exa
mple that combines both aspects is safe manual\nmemory management\, much i
n the style that the Rust programming\nlanguage allows.\n\nThis is all pos
sible in the\, latest\, 9.0 release of GHC. However\nthese applications\,
using GHC 9.0's linear types require quite a\nbit of additional syntactic
bureaucracy\, compared to their unsafe\nequivalent. In this talk\, after i
ntroducing Haskell's linear\ntypes\, I'll present linear constraints\, a f
ront-end feature for\nlinear typing that decreases the bureaucracy of work
ing with\nlinear types. Linear constraints are implicit linear arguments\n
that are to be filled in automatically by the compiler. Linear\nconstraint
s are presented as a qualified type system\, together\nwith an inference a
lgorithm which extends OutsideIn\, GHC's\nexisting constraint solver algor
ithm. Soundness of linear\nconstraints is ensured by the fact that they de
sugar into Linear Haskell.\n
LOCATION:https://webconf.math.cnrs.fr/b/noa-p22-a7m
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Giuseppe Di Molfetta / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210318T143000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210318T153000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.518504627326
DESCRIPTION:Giuseppe Di Molfetta: Gauge-invariance in celullar automata an
d multi-scales analysis\n\nCellular Automata constitute the most establish
ed distributed model of computation on space-time grid. It is clearly phys
ics-like\, in the sense that it shares some fundamental symmetries such as
homogeneity (invariance of the physical laws in time and space)\, causali
ty\, and often reversibility. When a CA is invariant under a transformatio
n identically performed at every point of the configuration space\, they a
re said to have a global symmetry. Typical global symmetries include refle
ctions\, rotations\, time inversion. Local symmetries\, the cornerstone of
gauge theories\, is a stronger constraint. I will provide a constructive
method\, a step-by-step procedure\, to make cellular automata invariant un
der the local action of a gauge group and the notion of gauge-equivalence
will be formalized. Then\, I will extend such results into the Quantum rea
lm by means of a concrete example. In conclusion\, I will discuss how such
discrete time and discrete space gauge invariant automata can be describe
d at larger scale\, e.g. by differential equations\, with and without info
rmation loss.\n
LOCATION:https://ecolepolytechnique.zoom.us/j/82016424508
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Niccolò Veltri / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210315T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210315T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.0178459342616
DESCRIPTION:Niccolò Veltri: Proof Theory of Skew Monoidal Categories\n\n(
Joint work with Tarmo Uustalu and Noam Zeilberger)\n\nThe skew monoidal ca
tegories of Szlachányi are a weakening of\nmonoidal categories where the
three structural laws of left and\nright unitality and associativity are n
ot required to be\nisomorphisms but merely transformations in a particular
\ndirection. In this talk\, we show that the free skew monoidal\ncategory
on a set of generating objects can be concretely\npresented as a sequent c
alculus. This calculus enjoys cut\nelimination and admits focusing\, i.e.
a subsystem of canonical\nderivations\, which solves the coherence problem
for skew monoidal\ncategories.\n\nWe also develop sequent calculi for par
tially normal skew\nmonoidal categories\, which are skew monoidal categori
es with one\nor more structural laws invertible. Each normality condition\
nleads to additional inference rules and equations on them. We\nprove cut
elimination and we show that the calculi admit\nfocusing. The result is a
family of sequent calculi between those\nof skew monoidal categories and (
fully normal) monoidal\ncategories. On the level of derivability\, these d
efine 8\nweakenings of the (unit\,tensor) fragment of intuitionistic\nnon-
commutative linear logic.\n\nIf time allows it\, we briefly discuss the pr
oof theory of skew\nprounital closed categories. These are variants of the
skew\nclosed categories of Street where the unit is not\nrepresented. Ske
w closed categories in turn are a weakening of\nthe closed categories of E
ilenberg and Kelly where no structural\nlaw is required to be invertible a
nd the presence of a monoidal\nstructure is not required.\n
LOCATION:https://webconf.math.cnrs.fr/b/noa-p22-a7m
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Constantin Enea / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210310T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210310T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.750002069259
DESCRIPTION:Constantin Enea: Automated Formal Testing of Transactional Dat
abases and Applications\n\nTransactions simplify concurrent programming by
enabling computations on shared data that are isolated from other concurr
ent computations and are resilient to failures. Modern databases provide d
ifferent isolation levels for transactions corresponding to different trad
eoffs between consistency and availability. The weaker the isolation level
\, the more behaviors a database is allowed to exhibit and it is up to the
developer to ensure that their application can tolerate those behaviors.\
n\nI will present a series of recent results that concern the problem of t
esting transactional databases and database-backed applications. First\, I
will focus on the problem of checking whether a given execution of a tran
sactional database adheres to some isolation level\, showing that isolatio
n levels like read committed\, read atomic\, and causal consistency are po
lynomial-time checkable while prefix consistency and snapshot isolation ar
e NP-complete in general. These results complement a previous NP-completen
ess result concerning serializability. Moreover\, in the context of NP-com
plete isolation levels\, we devise algorithms that are polynomial time ass
uming that certain parameters in the input executions\, e.g.\, the number
of sessions\, are fixed. Second\, I will present MonkeyDB\, a mock storage
system for testing database-backed applications. MonkeyDB supports a Key-
Value interface as well as SQL queries under multiple isolation levels. It
uses a logical specification of the isolation level to compute\, on a rea
d operation\, the set of all possible return values. MonkeyDB then returns
a value randomly from this set. We show that MonkeyDB provides good cover
age of weak behaviors\, which is complete in the limit.\n
LOCATION:https://webconf.math.cnrs.fr/b/sam-tq6-hwg
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Giulio Guerrieri / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210301T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210301T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.697704440945
DESCRIPTION:Giulio Guerrieri: Understanding the lambda-calculus via linear
ity and rewriting.\n\nThe lambda-calculus is the model of computation unde
rlying functional programming languages and proof assistants. Actually\, t
here are many lambda-calculi\, depending on the evaluation mechanism (e.g.
\, call-by-name\, call-by-value\, call-by-need) and computational feature
that the calculus aims to model (e.g.\, plain functional\, non-determinist
ic\, probabilistic\, infinitary).\n\nThe existence of different paradigms
is troubling because one apparently needs to study the theory and semantic
s of each one separately.\n\nWe propose a unifying meta-theory of lambda-c
alculi\, where the study is rooted on a unique core language\, the bang ca
lculus\, a variant of the lambda-calculus inspired by linear logic: a bang
operator marks which resources can be duplicated or discarded.\n\nThe ban
g calculus subsumes both call-by-name and call-by-value. A property studie
d in the bang calculus is automatically translated in the corresponding pr
operty for the call-by-name lambda-calculus and the call-by-value lambda-c
alculus\, thanks to two different embeddings of the lambda-calculus in the
bang calculus. These embeddings are grounded on a proof theory: they are
an adaptation of Girard's two translations of intuitionistic logic into li
near logic.\n\nAdvanced computational features are usually obtained by add
ing new operators to a core language. Instead of studying the operational
properties of the extended language from scratch\, we propose a simple met
hod to study them modularly: if an operational property holds in the core
language and in the new operators separately\, then a simple test of good
interaction between core language and new operators guarantees that the pr
operty lifts to the whole extended language. This approach is first develo
ped in abstract rewriting systems.\n
LOCATION:https://webconf.math.cnrs.fr/b/noa-p22-a7m
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ambroise Lafont / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210222T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210222T113000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.672676103554
DESCRIPTION:Ambroise Lafont: Mathematical specifications of programming la
nguages via modules over monads\n\nResearch in the field of programming la
nguages traditionally relies on\na definition of syntax modulo renaming of
bound variables\, with its associated operational semantics. We are inter
ested in mathematical\ntools allowing us to automatically generate syntax
and semantics from\nbasic data. We pay particular attention to the notion
of substitution\,\nusing the categorical notions of monads and modules ove
r them.\nLanguages with variable binding\, such as the pure lambda calculu
s\, are\nmonads on the category of sets. We provide a further notion of\nt
ransition monads which takes into account the operational semantics.\nWe
give examples of specifications for transition monads\, in the\nspirit of
Initial Semantics\, where an object is characterized by some\ninitiality p
roperty in a suitable category of models.\n
LOCATION:https://webconf.math.cnrs.fr/b/noa-p22-a7m
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Miki Hermann / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210218T143000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210218T153000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.310988704593
DESCRIPTION:Miki Hermann: Logical Analysis of Data\n\nWe show how to cope
with Big Data by means of Automated Deduction. We generate a Horn or a bij
unctive formula from sets of positive and negative tuples T and F\, respe
ctively These sets of tuples have been previously shortened to a locally m
inimal length\, provided that the two sets T and F keep an empty intersect
ion. Since the problem to find the minimal length is an NP-optimization pr
oblem\, we apply different approximation strategies. We also apply two app
roaches to formula production: (1) the LARGE approach\, where only tuples
of F falsify the produced formula\, and (2) EXACT\, where only tuples of T
satisfy the formula. In case of the large approach we apply a set cover
approximation algorithm to keep the minimal set of clauses falsifying all
tuples from the set F. The produced formula can be used to further charact
erize subsequent sets of tuples and identify their membership among the tr
ue or false examples. The whole system\, called MCP for Multiple Character
ization Problem\, has been implemented and can be found at .\n\n(research done in collaboration with Gernot Sal
zer\, Technische Universität Wien\, Vienna\, Austria)\n
LOCATION:https://cnrs-nqa.my.webex.com/cnrs-nqa.my-en/j.php?MTID=m756d7af4
63e4bd67a15d975d98225be4
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Uli Fahrenberg / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210217T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210217T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.0355422113558
DESCRIPTION:Uli Fahrenberg: Generating Posets Beyond N\n\nWe introduce ipo
sets - posets with interfaces - equipped with a novel gluing composition a
long interfaces and the standard parallel composition. We study their basi
c algebraic properties as well as the hierarchy of gluing-parallel posets
generated from singletons by finitary applications of the two compositions
. We show that not only series-parallel posets\, but also interval orders\
, which seem more interesting for modeling concurrent and distributed syst
ems\, can be generated\, but not all posets. Generating posets is also imp
ortant for constructing free algebras for concurrent semirings and Kleene
algebras that allow compositional reasoning about such systems.\n
LOCATION:https://webconf.math.cnrs.fr/b/sam-tq6-hwg
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Daniel Murfet / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210208T093000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210208T103000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.924515441817
DESCRIPTION:Daniel Murfet: Gentzen-Mints-Zucker duality: sequent calculus
vs λ-calculus\n\nI will report on joint work with Will Troiani\, in which
we revisit Howard’s work on the Curry-Howard correspondence and interpr
et it as an isomorphism between a category of proofs in intuitionistic seq
uent calculus and a category of terms in simply-typed λ-calculus.\nSome v
ersion of this is known to the experts due to work of Mints\, Zucker and o
thers\, but not for Gentzen’s original calculus.\nI will explain our tec
hnical contributions to the understanding of normal forms of sequent calcu
lus proofs\, and our view that the fundamental duality expressed is not be
tween “proofs and programs” but between local and global presentations
of a logico-computational structure.\n
LOCATION:https://webconf.math.cnrs.fr/b/noa-p22-a7m
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Matteo Acclavio / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210201T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210201T150000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.378147124299
DESCRIPTION:Matteo Acclavio: Games for constructive modal logics\n\nConstr
uctive modal logics are extensions of intuitionistic propositional logic w
ith certain modal axioms. Many proof systems are known for these logics\,
but the only available denotational semantics is defined by means of an ab
stract construction\, based on the quotient of their lambda terms.\n\nThe
general aim of our work is to define a game semantics for constructive mod
al logics. In this talk I will define the winning strategies for a formula
and show the correspondence between winning strategies and proofs. I will
show how winning strategies can be defined as the projection of specific
paths in a graphical proof system defined for this purpose - combinatorial
proofs.\n\n(this talk is based on a joint work with Davide Catta and Lutz
Strassburger)\n
LOCATION:https://webconf.math.cnrs.fr/b/noa-p22-a7m
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Robin Piedeleu / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210127T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210127T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.468870949821
DESCRIPTION:Robin Piedeleu: A diagrammatic axiomatisation of finite-state
automata\n\nIn this talk I will present a fully diagrammatic approach to t
he theory of finite-state automata\, based on reinterpreting their usual s
tate-transition graphs as string diagrams. Moreover\, I will give an equat
ional theory that completely axiomatises language equivalence in this new
setting. The proposed axiomatisation is finitary--- a result which is prov
ably impossible to obtain for the usual one-dimensional syntax of regular
expressions.\n
LOCATION:https://webconf.math.cnrs.fr/b/sam-tq6-hwg
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
BEGIN:VEVENT
SUMMARY:Maxime Lucas / Proofs and Algorithms seminar
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210113T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210113T120000
DTSTAMP;VALUE=DATE-TIME:20241107T115424Z
UID:0.805456032519
DESCRIPTION:Maxime Lucas: Abstract rewriting Internalised\n\nThere are two
historical trends in rewriting theory: "abstract rewriting"\, where one r
ewrites terms\, and "algebraic rewriting"\, where one rewrites linear comb
inations of terms. Although the two theories enjoy similar results\, there
are subtle differences that prevent the development of a unified theory:
for example in algebraic rewriting any reflexive relation is both symmetri
c and transitive.\nIn this talk we present a generic framework to study re
writing in a category C satisfying some suitable hypothesis. In the case C
= Set we recover abstract rewriting\, while algebraic rewriting correspon
ds to the case where C is the category of vector spaces. In this framework
\, we express notions of termination\, confluence and local confluence usi
ng a notion of rewriting strategy\, and prove an analogue of Newman's Lemm
a. Finally\, we hint at the higher dimensional analogue of this framework\
, with a view towards homotopy.\n
LOCATION:https://webconf.math.cnrs.fr/b/sam-tq6-hwg
ORGANIZER:MAILTO:samuel.mimram@lix.polytechnique.fr
END:VEVENT
END:VCALENDAR