After having skipped the 2020 edition due to both the sars-cov-2 pandemics and our hopes of organising a physical event after the first wave… here we are!

This year the workshop aims at making as many PPS members as possible speak about research topics and problems that they consider worthwhile.

You can find below the details of the talks.

If you have any question, do not hesitate to contact the organisers: G. Bernardi, C. Faggian, H. Herbelin, A. Saurin

On-line rooms

Relax room: https://gather.town/app/sPyXHQeTooLDzEO5/pps

Talk room for March 22nd (any password works): https://galene.org:8443/group/seminaire-pps

Talk room for the other days: https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-tje-nwj-dtk

Seminar room for the other days: https://galene.org:8443/group/seminaire-pps

13h45 On-line welcome / gathering in the relax room

14h00 · J. Chroboczek · Galène, un serveur de vidéoconférence libre

14h20 · H. Férée · Implicit Complexity for Higher-Order Functions

14h40 · B. Delcroix · Posets d'espèces / Species posets

15h00 — Coffee break in the relax room

15h10 · A. Saurin · Sur la Séquentialisation et la Construction de Réseaux de Preuves / On Proof-Net Search & Sequentialization

15h30 · M. Pagani · Automatic Differentiation in PCF

15h50 · P. Gaucher · Moore flows

16h10 — Coffee break in the relax room

16h20 · A. Bucciarelli · An algebraic theory of clones

16h40 · G. Bernardi · Flaky tests, informally

17h — End of the first day

10h30 · Morning seminar · C. Keller · SMTCoq: safe and efficient automation in Coq

13h45 On-line welcome / gathering in the relax room

14h00 · A. De · Provability of some fixed-point logics

14h20 · N. Jeannerod · Verification of Shell Scripts Performing File Hierarchy Transformations (PhD trailer)

14h40 · A. Spiwack · Linear types for the masses

15h00 — Coffee break in the relax room

15h10 · J. Krivine · Implementing a smart contract for the Ethereum blockchain: a short walk into a Dark Forest

15h30 · D. Petrișan · Combining probabilistic and non-deterministic choice via weak distributive laws

15h50 · L. Peyrot · The Spirit of Node Replication

16h10 — Coffee break in the relax room

16h20 · T. Ehrhard · Examples of computations in probabilistic coherence spaces

16h40 · T. Zimmermann · A model of community organization for the long-term maintenance of an ecosystem's packages

17h — End of the second day

13h45 On-line welcome / gathering in the relax room

14h00 · R. Nollet · Induction and coinduction in Multiplicative Additive Linear Logic

14h20 · L. Guetta · Looking for models of Homotopy types

14h40 · E. Gallego · Incremental Type-Checking of Coq Documents

15h00 — Coffee break in the relax room

15h10 · A. Guatto · Modalities and Parametric Right Adjoints

15h30 · P. Letouzey · Studying Regexps in Coq : Brzozowski, Antimirov and trying to prove the ml-ulex tool

15h50 · H. Herbelin · Effectful proof theory and beyond

16h10 — Coffee break in the relax room

16h20 · R. Crubillé · On higher-order cryptography

16h40 · C. Gonzalez · Blockchain smartcontracts out of spreadsheets

17h — End of the third day

17h00 Eva farewell get-together in this zoom room

10h30 · Morning seminar · P-E. Dagand · A Programming Model for Transiently-Powered Systems

13h45 On-line welcome / gathering in the relax room

14h00 · G. Curzi · Combining cyclic proofs and implicit complexity

14h20 · C. Faggian · Asymptotic normalization

14h40 · C. Leena Subramaniam · Parametric right adjoint monads, analytic functors, and linear dependent types

15h00 — Coffee break in the relax room

15h10 · AG scientifique

17h — Virtual apéro in the relax room

Galène (https://galene.org) est un serveur de vidéoconférence que j'ai écrit durant le premier confinement français, lorsque la mairie de Paris nous interdisait de sortir de jour de peur qu'on s'amuse mieux qu'eux.

Dans cet exposé, je vous raconterai pourquoi j'ai écrit mon propre serveur de vidéoconférence, comment j'ai fait, et comment les gens s'en servent. Je dirai aussi quelques mots sur les avantages des systèmes auto-hébergés (self-hosted), en évitant dans la mesure du possible de vexer les gens (certains de mes meilleurs amis utilisent Gmail).

Amongst other things, Implicit Complexity aims at helping us better understand complexity classes by obtaining characterisations of various kinds. Besides that, the notion of complexity for higher-order functions is just barely defined, let alone understood. We will here recall the current state of a specific kind of Implicity complexity technique, namely function algebras, and present the motivations and challenges behind its generalisation to functions of order 3 and more.

Les posets sont des ensembles munis d'un ordre partiel. Les espèces (de structure), introduites par Joyal dans les années 1980, sont des plans de constructions qui permettent de fabriquer des arbres ou des listes à partir de briques interchangeables. Après une présentation des deux protagonistes, je vous ferai visiter différents lieux où ils se cotoient et interagissent. Nous nous arrêterons notamment sur les posets de partition et de Tamari (et associaèdres associés).

Posets are Partially Ordered SETS. Species of structure (introduced in the 80s by Joyal) are installation instructions enabling qualified persons to build trees or lists from interchangeable elementary pieces. After a brief introduction of the two lads, we will go on a sightseeing tour of (some of) their meeting places. Two of the main stops will be partition posets and Tamari lattices (and associated associahedron).

Dans cet exposé, je m'intéresserai à la question de la construction de réseaux de preuves en logique linéaire, et j'expliquerai qu'en un certain sens, séquentialisation et construction de réseaux sont deux aspects du même phénomène.

Les réseaux de preuves sont des structures logiques où l'ordre des inférences a été (partiellement) oublié: les arbres du calcul des séquents deviennent alors des graphes de structures de preuves. Une conséquence est que la correction logique de l'objet de preuve n'est plus une propriété inductive locale, mais une propriété globale, qui peut être analysée topologiquement: certains graphes sont logiquement corrects (et ils peuvent alors être séquentialisés en une preuve du calcul des séquents) quand d'autres ne le sont pas. On définit ainsi des critères de correction qui caractérisent les graphes corrects (qu'on appelle alors des réseaux de preuves) des autres.

Pour étudier la construction de réseaux de preuves, on se placera dans un système logique étendu de structures d'épreuves (ou de para-preuves) en considérant une inférence spéciale permettant de représenter les preuves en construction (ou preuves ouvertes, ou ayant des buts non résolu): il s'agit d'un axiome généralisé similaire au démon de la Ludique.

Dans ce cadre élargi, on passera en revue trois critères de correction classiques (Danos-Regnier, Contractibilité et Parsing) dont on mettra en évidence la signification logique: - le premier se réexprime comme un critère interactif: une structure de preuve est correcte si elle passe certains tests; - le second correspond à une séquentialisation distribuée des structures d'épreuves; - le troisième, qui est une spécialisation de la contractibilité, permet d'aborder la question de la construction de réseaux de preuve dont on parlera dans la fin de l'exposé.

–

In this talk, I will focus on the question of proof-net construction in linear logic and I will explain that sequentialization and proof-net construction can be viewed as two faces of the same coin.

Proof-nets are deductive structures in which the order of inference has been (partially) forgotten: sequent calculus derivation trees become graphs of proof structures. As a consequence, logical correctness is not a local, inductive property anymore, but a global one, which may be investigated using topological arguments: some graphs are logically correct (and they can be sequentialized into a sequent proof) while some are not. One defines correctness criteria in order to characterize correct proof structures (aka. proof-nets) from incorrect ones.

To study proof-net construction, one will consider an proof system extended to para-proof structures by considering a new inference representing proof-searches (or open proofs, that is with unsolved goals): this inference is a generalized axiom similar to Ludics' daimon.

In this extended framework, one shall first review three classical correctness criteria (Danos-Regnier, Contractibility and Parsing) in order to unveil their logical significance: - the first one is an interactive criterion: a para-proof structure is correct if it passes some tests; - the second one corresponds to a form of distributed sequentialization of para-proofs; - the third one, which is a specialization of contractibility, will guide us to the issue of proof-net construction that we shall discuss in the last part of the talk.

We study the correctness of automatic differentiation (AD) in the context of a higher-order, Turing-complete language (PCF with real numbers), both in forward and reverse mode. Our main result is that, under mild hypotheses on the primitive functions included in the language, AD is almost everywhere correct, that is, it computes the derivative or gradient of the program under consideration except for a set of Lebesgue measure zero. Stated otherwise, there are inputs on which AD is incorrect, but the probability of randomly choosing one such input is zero. Our result is in fact more precise, in that the set of failure points admits a more explicit description: for example, in case the primitive functions are just constants, addition and multiplication, the set of points where AD fails is contained in a countable union of zero sets of (non-null) polynomials.

I managed to prove that the q-model structures of multipointed d-spaces (a variant of Grandis' d-spaces) and of flows (a.k.a small semicategories enriched over topological spaces) are Quillen equivalent. The obvious functor from multipointed d-spaces to flows is neither a left nor a right adjoint so it was not a possible candidate, even if its left derived functor already induces an equivalence of categories between the homotopy categories. I have to introduce an intermediate category, the Moore flows, and I can then find a zig-zag of Quillen equivalences between multipointed d-spaces and flows. The idea of introducing Moore flows seems to be a priori absurd since it consists of adding length to morphisms. This well-known method in algebraic topology, introduced by Moore, is a workaround to the fact that the composition of continuous paths is not strictly associative. It becomes strictly associative by considering continuous paths with length. But the composition of morphisms in flows is already strictly associative… In this talk, I will describe the zig-zag of Quillen equivalences.

I will present joint work with Antonino Salibra dealing with the notion of “clone of operations”, originated in universal algebra and largely used (without the name) in computer science. Before sketching our algebraic axiomatisation of clones, I will provide an overview of some of these applications.

A test that can pass and fail in different runs of the same software is called flaky. Not surprisingly, flaky these are a major industrial issue in software testing.

In this talk I we first give overview flaky tests and their impact, and then we sketch the formal methods we propose to tackle the problem in a provably sound manner.

The subject of the SMTCoq project is to significantly enhance automation in the Coq proof assistant. At the heart of SMTCoq is a Coq plugin that offers a way to use automatic provers with the same degree of trust as Coq itself. On top of it, we define a framework to progressively encode Coq's logic into first-order logic, through modular and fine-grained logical transformations that can be composed. Our objective is to obtain automatic while expressive tactics for Coq.

In this talk, I will concisely introduce the communication between Coq and external provers, before presenting the new framework of logical transformations. I will report on work in progress of examples of transformations in this framework.

This is joint work with Valentin Blot, Louise Dubois de Prisque and Pierre Vial.

In this short talk, I will give a high level introduction to the non-wellfounded proof theory of mu-calculus and discuss some questions on the provability of a given sequent. Structural rules are crucial players here. In order, to fully understand their role, we examine the same problems in the linear setting. This is an ongoing work with Alexis Saurin and Anupam Das.

In this talk, I will present a trailer of my Ph.D. defence, “Verification of Shell Scripts Performing File Hierarchy Transformations”. I will present the problem we are trying to solve (the quality assurance of Debian software packages) and an overview of how we solve it, as well as a few results.

I’ve been working, in the past few years, at extending a production-grade compiler (namely GHC, the main Haskell compiler) with linear types. This has the potential of letting linear-logic-style type systems touch a wider public. I’ll be speaking about my experience, and will discuss the newest results on making linear typing easier to use: namely linear constraints, by which we extend Haskell’s type class mechanism to linear logic.

Implementing smart contract is rather straightforward, but anticipating how it will behave once deployed on a blockchain requires novel ways (at least for me) of thinking about reactive systems. I will discuss the issue of « trusting the code » , « reentrancy », and « slippage ».

It is a well known result that there is no distributive law between the powerset monad and the finite distribution monad. In this talk, I will briefly present a weak distributive law between these monads and a canonical way of composing them. Then I  discuss ongoing extensions of this work to a continuous setting. This is joint work with Alexandre Goy.

Abstract: We define and study a term calculus implementing higher-order node replication. It is used to specify two different (weak) evaluation strategies: call-by-name and fully lazy call-by-need, that are shown to be observationally equivalent by using type theoretical technical tools.

Sans entrer dans les définitions techniques, je montrerai quelques interprétations de programmes fonctionnels comme fonctions analytiques entre espaces cohérents probabilistes et je ferai quelques calculs sur ces interprétations.

In this talk, I present a work-in-progress qualitative study with Jean-Rémy Falleri (LaBRI) about an emerging model of community organization for package maintenance. I have discovered this type of organizations during my PhD, first in the Elm ecosystem, then in several other package ecosystems. These community organizations create a shared space where key ecosystem packages (that would otherwise risk of being abandoned) can be hosted and members of the ecosystem can collaborate in maintaining them. We are adopting a qualitative methodology called “grounded theory”, which originates from sociology, to study these organizations and figure out their key characteristics. Based on this organization model, I have founded the coq-community organization in 2018, and this is now a key component of the Coq ecosystem, as it has attracted more than 30 maintainers and hosts more than 50 packages.

Disclaimer : Despite the title, my talk is not about “homotopy type theory”. The meaning “homotopy type” is the one from homotopy theory, which is : “space up to homotopy”.

In this talk I will present a current interest of mine which is that of finding models for homotopy types. I will first explain precisely what this means and then mention Grothendieck's homotopy conjecture which states that (his definition of) weak ∞-groupoids model homotopy types. Finally, I will  very shortly present the notion of n-fold groupoids and explain how they could provide a model for homotopy n-times.

The interactive proof assistant Coq allows provides a strong foundational basis on top of which complex proofs of mathematical theorems and algorithms have been built.

A key feature of such proofs is their large size, thus checking that such proofs are valid requires large amounts of computational power and time. This is in conflict with the needs for their effective development, which is usually done via small, incremental changes.

As of today, incremental checking of Coq proofs is done at file-level granularity, either using the `make` build system, or the more recent `dune`, which provides some more advanced features such as global caching of build rules, sandboxing, or hash-based target validation.

While file-level granularity can significantly reduce incremental checking time, it is still not enough for large projects, CI, and user interfaces, use cases that for different reasons, do suffer from having to re-check complete files if a modification in the dependency tree does occur.

In this talk we will present work on `flèche`: an intra-file incremental type checking engine for Coq. Flèche understand dependencies among the objects of a Coq document, and will only re-check parts that are needed, providing large speedups w.r.t. file-level granularity in several interesting use cases.

As a wise man said, modal logics are domain-specific logics: various philosophical, mathematical, or computational situations suggest modal extensions to type theory. Each such extension requires careful integration with the syntactic structure of the language, lest its delicate metatheory should falter. I will present recent work by Gratzer, Cavallo, Kavvos, Birkedal and myself proposing a uniform theory of modal extensions based on the category-theoretical notion of parametric right adjoint.

Joint work with Yann Régis-Gianas.

I'll present the current state of a Coq formalization done with Yann, where we revisited some of the theory of regular expressions and automata : Brzozowski derivatives and the Brzozowski finiteness theorem, Antimirov partial derivatives, and how to build and justify an automata from all that. Then I'll focus on the ml-ulex tool (an “ocamllex”-like from the SML/NJ community, nicely described in [1]) and I'll describe how we tried proving this ml-ulex engine in Coq. And currently, failed…

[1] Regular-expression derivatives re-examined, S. Owens, J. Reppy, A. Turon, JFP 2009

I will give a condensed overview of typical questions I'm interested in:

• using exceptions to compute with Markov's principle
• using lazy evaluation of coinductive streams and control to compute with the axiom of dependent choices (with É. Miquey)
• using memory to nicely compute with the theorem of Tarski completeness
• using Lisp's quote to compute with the axiom of extensional choice (with A. Miquel and F. Castro)
• using parametricity to compute with extensional equality (Cubical Type Theory, with H. Moeneclaey)

I will end with a short description of the objectives of πr²'s submitted followup, Picube

• fundamental structures of logic and of mathematical reasoning
• differential and probabilistic tools for programming, reasoning and learning
• architecture and design of a proof assistant for the working mathematician
• formalisation and linguistics of mathematics
• higher dimensional algebra and synthetic homotopy theory

Type-two constructions abound in cryptography: adversaries for encryption and authentication schemes, if active, are modeled as algorithms having access to oracles, i.e. as second-order algorithms. But how about making cryptographic schemes themselves higher-order? This work gives an answer to this question, by first describing why higher-order cryptography is interesting as an object of study, then showing how the concept of probabilistic polynomial time algorithm can be generalized so as to encompass algorithms of order strictly higher than two, and finally proving some positive and negative results about the existence of higher-order cryptographic primitives, namely authentication schemes and pseudorandom functions. (joint work with Boaz Barak & Ugo Dal Lago)

I will talk about my ongoing work as a PhD candidate at the IRIF and Nomadic Labs. This research focuses on providing a tool to design smartcontracts using spreadsheet software as a user interface. The end goal is to design and implement a certified compiler from spreadsheets to the Michelson smart-contratcs language, relying on the recent of work about static differentiation of lambda-calculus in ESOP'19 by Yann Régis-Gianas and his coauthors.

Transiently-powered systems featuring non-volatile memory as well as external peripherals enable the development of new low-power sensor applications. However, as programmers, we are ill-equipped to reason about systems where power failures are the norm rather than the exception. A first challenge consists in being able to capture all the volatile state of the application –external peripherals included– to ensure progress. A second, more fundamental, challenge consists in specifying how power failures may interact with peripheral operations. In a joint work with Rémi Oudin, Delphine Demange, Gautier Berthou and Tanguy Risset, we have proposed a formal specification of intermittent computing with peripherals, an axiomatic model of interrupt-based checkpointing as well as its proof of correctness, machine-checked in the Coq proof assistant. However, this result assumes that the system is able to maintain a shadow copy of the external devices it interacts with. Perhaps surprisingly, this could be an opportunity to adopt an algebraic treatment of external peripherals.

Cyclic proofs (i.e. non-wellfounded but regular proofs) have received growing interest in the literature, and have been proposed as an alternative setting for studying (co)inductive reasoning. However, little is known about the complexity-theoretical aspects of cyclic proofs, which very often exhibit quite convoluted loop structures. This talk is an attempt to bridge the gap between implicit complexity and cyclic proofs. We study a cyclic proof system based on Hofmann’s SLR (Safe Linear Recursion), and we look for suitable proof-theoretical constraints able to reduce the complexity of loops and to capture some interesting complexity classes, such as ELEMENTARY and PTIME. This is joint work with Anupam Das.

I will give some examples of rewriting where termination is asymptotic, that is, the result appears as a limit, as opposite to reaching a normal form in a finite number of steps. Probabilistic computation is a prime example: limits are here distributions over the possible outputs. However, asymptotic termination occurs in settings as diverse as effectful computation, streams, or infinitary lambda-calculi (where the limits are infinitary normal forms such as Boehm trees). I am interested in proof techniques for studying the operational theory of such systems.

Parametric right adjoint (pra) functors (and analytic functors, that can be understood as higher dimensional pra functors) on presheaf categories are multisorted term signatures “with arities” whose operations consume their input in a “linear” way. They strictly generalise the notion of stable functor (resp. analytic functor) from Set to Set.

I will present some ideas on how this could be thought of syntactically using dependent types and “linear” dependently typed term signatures. This is very much a work in progress—here be dragons!