==== Journées PPS 2019 ==== **// Programme préliminaire et liste des exposés disponibles ci-dessous.//** Chaque jour, l'accueil se fera à 9h et les exposés débuteront à 9h30. Les exposés et pauses cafés auront lieu en amphi Turing, les déjeuners à l'IRIF au troisième étage du bâtiment Sophie Germain. Deux exposés invités (Hugo Férée et Constantin Enea) dureront 1h (incluant la discussion) tandis que les autres exposés dureront 30 minutes suivies de 10 à 15 minutes de questions. Une réunion du pôle PPS aura lieu lundi après-midi. //9h — Café & croissant collectif// /* ** xxhxx -- xxhxx ** · nom · {{lien|titre}} */ ** 9h30 -- 10h ** · Thierry Joly · Vers une P(reuve) P(urement) S(yntaxique) du 2nd Théorème d'Incomplétude de Gödel ** 10h15 -- 10h45 ** · Ralf Treinen · A Decade of Applying Formal Methods to Free Software //11h — Pause café// ** 11h15 -- 12h15 ** · Hugo Férée · Complexité des fonctions d'ordre supérieur ** 12h15 -- 12h45 ** · Paul Ruet · Théorie géométrique des groupes et complexité //13h — Buffet au lobby du 3ème étage// ** 14h -- 15h ** · AG pôle PPS //15h — Pause café// ** 15h30 -- 16h ** · Adrien Guatto · On an Extension of Lambek Calculus ** 16h15 -- 16h45 ** · Abhishek De · Infinets : The parallel syntax of non-wellfounded proof theory //17h — Fin de la journée// //9h — Café & croissant collectif// ** 9h30 -- 10h ** · Chaitanya Leena Subramaniam · Dependent type theories as "cellular" Lawvere theories ({{chait.pdf|slides}}) ** 10h15 -- 10h45 ** · Axel Osmond · Construction générale des foncteurs spectraux ({{osmond.pdf|slides}}) //11h — Pause café// ** 11h15 -- 12h15 ** · Constantin Enea · Reasoning About Replicated Data Types ({{enea.pdf|slides}}) ** 12h15 -- 12h45 ** · Yann Régis-Gianas · Implementation and Verification of Modular Effectful Systems in Coq using FreeSpec ({{yrg.pdf|slides}}) //13h — Buffet au lobby du 3ème étage// ** 14h -- 14h30 ** · Christine Tasson · Résultats et problèmes en sémantique des langages de programmation probabiliste ({{tasson.pdf|slides}}) ** 14h45 -- 15h15 ** · Michele Pagani · Backpropagation in the Simply Typed Lambda-calculus with Linear Negation // 15h30 — Pause café // ** 15h45 -- 16h15 ** · Pierre Letouzey · Certification Coq d'un cours de logique de master ({{letouzey.pdf|slides}}) ** 16h30 -- 17h ** · Antonio Bucciarelli · n-dimensional Boolean algebras ({{buccia.pdf|slides}}) //17h15 — Fin des journées// === Liste des Exposés === /* */ /* Antonio Bucciarelli · n-dimensional Boolean algebras*/ Résumé : n-dimensional Boolean algebras (nBA) generalise BA to the case of n perfectly symmetric truth values. They arise as particular cases of simpler structures called n-dimensional Church Algebras (nCA) This talk aims at providing an overview of the algebraic structure and propositional calculus of nBAs, and starts with an application of 2CAs to the study of models of the untyped lambda-calculus. /* Abhishek De · Infinets : The parallel syntax of non-wellfounded proof theory */ Résumé : Logics based on the mu-calculus are used to model inductive and coinductive reasoning and to verify reactive systems. A well structured proof-theory is needed in order to apply such logics to the study of programming languages with (co)inductive data types and automated (co)inductive theorem proving. While traditional proof system suffers some defects, non-wellfounded (or infinitary) and circular proofs have been recognized as a valuable alternative, and significant progress have been made in this direction in recent years. Such proofs are nonwellfounded sequent derivations together with a global validity condition expressed in terms of progressing threads. The current work investigates a discrepancy found in such proof systems, between the sequential nature of sequent proofs and the parallel structure of threads: various proof attempts may have the exact threading structure while differing in the order of inference rules applications. The paper introduces infinets, that are proof-nets for non-wellfounded proofs in the setting of multiplicative linear logic with least and greatest fixed-points and study their correctness and sequentialization. (This is joint work with Alexis Saurin.) /* Constantin Enea · Reasoning About Replicated Data Types */ Résumé : Modern computer software is typically built with specialized concurrent or replicated objects, which encapsulate low-level shared-memory accesses into higher-level abstract data types. Typical examples include the concurrent collections of Java, distributed key-value stores like MongoDB, Cassandra, and Amazon S3, and the more recent conflict-free replicated data types (CRDTs) implemented in AntidoteDB and Riak. These objects are designed to behave according to certain consistency criteria like linearizability, eventual or causal consistency. In this talk, we give an overview of recent results concerning the semantics and the verification of such objects, focusing on the theoretical limits of testing and full functional verification. /* Hugo Férée · Complexité des fonctions d'ordre supérieur */ Résumé : Contrairement à celle des programmes manipulant uniquement des données intrinsèquement finies (entiers, mots binaires, graphes, etc.), la complexité des calculs faisant intervenir des objets tels que les fonctions d'ordre supérieur, des structures de données co-inductives ou d'autres données infinies n'est pas toujours comprise, voire même définie. Je présenterai ici une proposition de définition de complexité pour les fonctions d'ordre supérieurs basée sur la sémantique des jeux, et en profiterai pour présenter succinctement les travaux (en complexité implicite et analyse récursive) qui m'ont amenés à cette thématique, et les pistes de recherche que je souhaite suivre à PPS à partir de ce point de départ. /* Philippe Gaucher · Six structures modèles pour l'homotopie dirigée */ Résumé : J'expliquerai comment construire à partir de la théorie des bifibrations six structures modèles en rapport avec l'homotopie dirigée. Et en rajoutant un petit ingrédient, j'expliquerai comment passer à 12 structures modèles. /* Adrien Guatto · On an Extension of Lambek Calculus */ Résumé : Lambek calculus originates from formal linguistics, and can retrospectively be understood as non-commutative intuitionnistic linear logic. It also turns out to be deeply related to type-checking problems for a certain class of functional programming languages. In this talk, I will present an extension of Lambek calculus motivated by the latter connection, and discuss ongoing work on its decision problem. /* Yves Guiraud et al · AG du pôle PPS */ Résumé : Le pôle PPS tiendra une AG pour désigner un nouveau ou une nouvelle responsable à l'occasion du départ d'Yves à l'IMJ. This is joint work by Yves Guiraud and other members of PPS. /* Thierry Joly · Vers une P(reuve) P(urement) S(yntaxique) du 2nd Théorème d'Incomplétude de Gödel */ Résumé : Souvent, on simplifie une preuve en généralisant ses outils. C'est peut-être ce qui pourrait arriver au second théorème d'incomplétude de Gödel par un usage plus soutenu des variables, tellement folles à lier qu'on ne s'y hasarde jamais trop. Pourtant, en généralisant la formule □F (= "F est démontrable") aux formules F ayant des variables libres, il semble possible d'en écourter drastiquement la preuve, au prix de la gestion de ces variables libres, et donc à lier. /* Chaitanya Leena Subramaniam · Dependent type theories as "cellular" Lawvere theories */ Résumé : (joint work with P. LeFanu Lumsdaine) Lawvere theories and (coloured) operads provide particularly nice representations for suitable algebraic theories with a given set of sorts, as monoids in certain categories of collections. We extend this to dependent type theories: For an inverse category C, we show how suitable “C-sorted type theories” may be viewed (1) as monoids in a category of collections, and (2) as generalised Lawvere theories in the sense of Berger–Melliès–Weber. Moreover, (essentially) every dependent type theory arises in this way. Inverse categories are known from homotopy theory, where they (or their opposite categories) provide a good notion of a category of "cells". Examples are the category of semi-simplices, the category of globes, the category of opetopes, etc. /* Pierre Letouzey · Certification Coq d'un cours de logique de master */ Résumé : Depuis une dizaine d'années, je m'occupe d'un cours de logique à destination de nos Master 1 : on y parle essentiellement de calcul des prédicats du 1er ordre façon déduction naturelle (avec contextes), de modèles classiques, et du théorème de complétude. Tout ceci suit toujours un (très bon) poly d'Alexandre Miquel. Dans cet exposé, je vais présenter la "traduction" Coq récente de ce poly. Evidemment, pour des théorèmes aussi standards, la motivation n'était pas tellement de garantir l'absence d'erreur dans les preuves d'origines. Par contre, les preuves Coq peuvent venir en complément de preuves au tableau devant les étudiants, soit comme référence lors des moments les plus délicats, soit au contraire pour justifier qu'on zappe certaines parties répétitives. De plus, la présentation des encodages Coq aux étudiants a permis de souligner le côté mécanisable de cette logique, avec à terme l'obtention d'un micro assistant de preuve. Cela fut également l'occasion d'un premier contact des étudiants avec Coq, ce qui est un des autres objectifs de ce cours. Enfin, Coq a également permis d'essayer différentes variantes (encodage avec nom ou "locally nameless", divers substitutions nommées, etc). À terme, on peut imaginer une utilisation plus interactive de ce développement par les étudiants (p.ex. exos de déduction naturelle avec Coq comme correcteur). La page du cours et le code du développement Coq: https://www.irif.fr/users/letouzey/edu/preuves / https://gitlab.math.univ-paris-diderot.fr/letouzey/natded /* Axel Osmond · Construction générale des foncteurs spectraux */ Résumé : Plusieurs dualités importantes en mathématiques, comme la dualité de Stone pour les treillis distributifs ou la dualité de Grothendieck pour les anneaux commutatifs, se trouvent être des exemples d'une même construction générale où à des objets de nature algébrique sont associés par un foncteur spectral des "espaces structurés", modulo un choix de "données locales" définissant une géométrie. Cette construction repose sur la notion clé de structure d'admissibilité, laquelle relie les objets algébriques à dualiser aux "objets locaux" de façon à exhiber ceux-ci comme les points des espaces duaux. Il s'agit d'une situation de "multireflexivité" où un défaut d'unicité dans une construction universelle fait que plusieurs objets locaux libres peuvent être associés à un même objet : le rôle du spectre est alors de rassembler ces différents candidats en un unique objet, modulo changement de topos. Dans cet exposé, j'expliquerai l'intuition derrière les différentes approches de cette construction où s'entrelacent théorie catégorique des modèles, topologie, systèmes de factorisation et théorie des topos. /* Michele Pagani · Backpropagation in the Simply Typed Lambda-calculus with Linear Negation */ Résumé : (Joint work with Alois Brunel and Damiano Mazza). Backpropagation is a classic automatic differentiation algorithm computing the gradient of functions specified by a certain class of simple, first-order programs, called computational graphs. It is a fundamental tool in several fields, most notably machine learning, where it is the key for efficiently training (deep) neural networks. Recent years have witnessed the quick growth of a research field called differentiable programming, the aim of which is to express computational graphs more synthetically and modularly by resorting to actual programming languages endowed with flow control operators and higher-order combinators, such as map and fold. In this work, we extend the backpropagation algorithm to a paradigmatic example of such a programming language: we define a compositional program transformation from the simply-typed lambda-calculus to itself augmented with a notion of linear negation, and prove that this computes the gradient of the source program with the same efficiency as first-order backpropagation. The transformation is completely effect-free and thus provides a purely logical understanding of the dynamics of backpropagation. /* Yann Régis-Gianas · Implementation and Verification of Modular Effectful Systems in Coq using FreeSpec */ Résumé : Many software systems interact with their environment: a typical application creates files, send datagrams through network sockets, and more generally traverses many software layers to achieve basic effectful mechanisms. To get strong guarantees about the execution of these systems, one can implement a software stack from the ground up using a proof assistant like Coq and prove every desired property along the way. Another plan would be to implement the system with a mixture of untrusted and certified modules, gradually extending the portion of certified code. This method shortens the path to getting runnable software but it requires modularity mechanisms for implementations, specifications, and proofs. FreeSpec is a Coq library and plugin that offers that kind of modularity mechanisms to implement, to verify and to compose effectful components. In this talk, we will present these mechanisms as well as several applications ranging from building secure hardware architectures to UNIX-style standalone programs. This is joint work with Thomas Letan, Vincent Tourneur, Guillaume Hiet and Pierre Chifflier. /* Paul Ruet · Théorie géométrique des groupes et complexité */ Résumé : Liens entre isopérimétrie et complexité du problème du mot (un théorème de Birget, Ol’shanskii, Rips et Sapir). /* Christine Tasson · Résultats et problèmes en sémantique des langages de programmation probabiliste */ Résumé : Les langages de programmation probabiliste sont utilisés pour décrire des modèles statistiques sans se soucier de l'implémentation des algorithmes d'inférence qui sont programmés dans le compilateur. Suivant cette idée, plusieurs langages de programmation, parfois fonctionnels, ont vu le jour, soulevant des problèmes pratiques (optimisation, efficacité) et théorique (comment combiner l'ordre supérieur avec les probabilités, quelle sémantique). Dans cet exposé, je présenterai les résultats (plus ou moins) récents en sémantique et les problématiques que nous aimerions aborder dans un futur (plus ou moins) proche. /* Ralf Treinen · A Decade of Applying Formal Methods to Free Software */ Résumé : We look at some of the past and ongoing works at the PPS lab, and later IRIF, on the application of formal methods to Free Software. We discuss how one can do research that is not only academically successful, but that is also accepted in the Free Software community. This talk will not attempt to cover all the results obtained in a series of research projects over the last years but rather pick some examples, look at cases where our tools where successfully applied, but also at cases where the success was not as initially expected.