BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Samuel Mimram//Proofs and Algorithms seminar//EN
X-WR-CALNAME:Proofs and Algorithms seminar
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:20230331T074251Z
UID:0.524479332908
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:20230331T074251Z
UID:0.815458612774
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:20230331T074251Z
UID:0.19455740915
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:20230331T074251Z
UID:0.284297038354
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:20230331T074251Z
UID:0.152532050353
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:20230331T074251Z
UID:0.287500421303
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:20230331T074251Z
UID:0.180504091011
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:20230331T074251Z
UID:0.344855075378
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:20230331T074251Z
UID:0.926942242854
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:20230331T074251Z
UID:0.0661398917502
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:20230331T074251Z
UID:0.864309028189
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:20230331T074251Z
UID:0.0343553295935
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:20230331T074251Z
UID:0.826899099922
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:20230331T074251Z
UID:0.470895757206
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:20230331T074251Z
UID:0.959221043643
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:20230331T074251Z
UID:0.255891338529
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:20230331T074251Z
UID:0.465927252824
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:20230331T074251Z
UID:0.177701285012
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:20230331T074251Z
UID:0.478254578563
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:20230331T074251Z
UID:0.510011080922
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:20230331T074251Z
UID:0.593984276948
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:20230331T074251Z
UID:0.777018875467
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:20230331T074251Z
UID:0.226544231512
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:20230331T074251Z
UID:0.874771531615
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:20230331T074251Z
UID:0.0441791697579
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:20230331T074251Z
UID:0.805207238849
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:20230331T074251Z
UID:0.433404669579
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:20230331T074251Z
UID:0.611798349727
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:20230331T074251Z
UID:0.645195263224
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:20230331T074251Z
UID:0.610264952916
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:20230331T074251Z
UID:0.0622845605094
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:20230331T074251Z
UID:0.258290736226
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:20230331T074251Z
UID:0.0747978630448
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:20230331T074251Z
UID:0.210312153232
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:20230331T074251Z
UID:0.998360240797
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:20230331T074251Z
UID:0.185727372702
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:20230331T074251Z
UID:0.00468401079073
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:20230331T074251Z
UID:0.814506313
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:20230331T074251Z
UID:0.641875298301
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:20230331T074251Z
UID:0.385325672247
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:20230331T074251Z
UID:0.150408972373
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:20230331T074251Z
UID:0.866361046331
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:20230331T074251Z
UID:0.141248682346
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:20230331T074251Z
UID:0.356007079152
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:20230331T074251Z
UID:0.357886512434
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:20230331T074251Z
UID:0.230362283692
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:20230331T074251Z
UID:0.531503067788
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:20230331T074251Z
UID:0.806899538693
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:20230331T074251Z
UID:0.914409812915
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:20230331T074251Z
UID:0.81991111805
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:20230331T074251Z
UID:0.389262593716
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:20230331T074251Z
UID:0.625591789419
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:20230331T074251Z
UID:0.787853774933
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:20230331T074251Z
UID:0.548143581281
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:20230331T074251Z
UID:0.872792977395
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:20230331T074251Z
UID:0.0144970574958
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:20230331T074251Z
UID:0.985869457335
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:20230331T074251Z
UID:0.378027466763
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:20230331T074251Z
UID:0.44510090594
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:20230331T074251Z
UID:0.961195005313
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:20230331T074251Z
UID:0.185238987387
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