BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Samuel Mimram//Proofs and Algorithms seminar//EN
X-WR-CALNAME:Proofs and Algorithms seminar
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:20220525T191910Z
UID:0.0510351870395
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:20220525T191910Z
UID:0.321104771427
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:20220525T191910Z
UID:0.869255840489
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:20220525T191910Z
UID:0.300767010126
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:20220525T191910Z
UID:0.323003310718
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:20220525T191910Z
UID:0.795013655863
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:20220525T191910Z
UID:0.875577862926
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:20220525T191910Z
UID:0.9648542164
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 regula
r languages according to their localisation \nwithin the internal structur
e of NC¹\, the class of languages decided by Boolean circuits of polynomi
al size\, logarithmic depth and with gates of constant fan-in. In some sen
se\, the search for such a classification concentrates most of the open qu
estions we have about the relationship between NC1 and its well-studied su
bclasses.\n\nWhile many questions are still open\, one of the greatest suc
cesses of this research endeavour has been the characterisation of the reg
ular languages in AC⁰\, the subclass of NC¹ corresponding to Boolean c
ircuits of polynomial length\, constant depth and with gates of unbounded
fan-in. This characterisation takes the form of a triple languages-algebra
-logic correspondence: a regular language is in AC0 if and only if its syn
tactic morphism is quasi-aperiodic if and only if it is definable in first
-order logic over words with linear order and modular predicates.\n\nIt is
natural to try to extend such results to classes of formal languages gre
ater than the class of regular languages. A well studied and robust such
class is given by visibly pushdown languages (VPLs): languages recognised
by pushdown automata where the stack-height-behaviour only depends on the
letters read from the input. Over the previous decade\, a series of work
s concentrated on the fine complexity of VPLs\, with several achievements
: one of those was a characterisation of the class of visibly counter lan
guages (basically VPLs recognised by visibly pushdown automata with only
one stack symbol) in AC⁰ by Krebs\, Lange and Ludwig. However\, the cha
racterisation of the VPLs in AC⁰ still remains open. \n\nIn this talk\,
I shall present a conjectural characterisation of the VPLs in AC⁰ obtai
ned with Stefan Göller at the Universität Kassel. It is inspired by the
conjectural characterisation given by Ludwig in his Ph.D. thesis as a gen
eralisation of the characterisation for visibly counter languages\, but th
at is actually false. In fact\, we give a more precise general conjectura
l characterisation that builds upon recognisability by morphisms into Ext-
algebras\, an extension of recognisability by monoid-morphisms proposed b
y Czarnetzki\, Krebs and Lange to suit the case of VPLs. This characterisa
tion classifies the VPLs into three categories according to precise condit
ions on the Ext-algebra-morphisms that recognise them:\n- those that are T
C⁰-hard\;\n- those that are in AC⁰\;\n- those that correspond to a wel
l-identified class of "intermediate languages" that we believe to be neith
er 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:20220525T191910Z
UID:0.663950129755
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:20220525T191910Z
UID:0.12324414296
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:20220525T191910Z
UID:0.747506820374
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:20220525T191910Z
UID:0.0588436029254
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:20220525T191910Z
UID:0.507857783309
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:20220525T191910Z
UID:0.999535423947
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:20220525T191910Z
UID:0.686404468889
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:20220525T191910Z
UID:0.509138696213
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:20220525T191910Z
UID:0.590758611101
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:20220525T191910Z
UID:0.322069295352
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:20220525T191910Z
UID:0.736675517081
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:20220525T191910Z
UID:0.997894250464
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:20220525T191910Z
UID:0.936158418241
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:20220525T191910Z
UID:0.858489352886
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:20220525T191910Z
UID:0.986685481204
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:20220525T191910Z
UID:0.195121375725
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:20220525T191910Z
UID:0.431992264818
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:20220525T191910Z
UID:0.378857505325
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:20220525T191910Z
UID:0.306417851406
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:20220525T191910Z
UID:0.737077292268
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:20220525T191910Z
UID:0.219487124114
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:20220525T191910Z
UID:0.929541974092
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:20220525T191910Z
UID:0.45097264681
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:20220525T191910Z
UID:0.339973003046
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:20220525T191910Z
UID:0.0347754763798
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:20220525T191910Z
UID:0.979313612946
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:20220525T191910Z
UID:0.451722722247
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:20220525T191910Z
UID:0.185139412931
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:20220525T191910Z
UID:0.602227818917
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:20220525T191910Z
UID:0.718995492801
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