Preuves, programmes et systèmes Jeudi 12 décembre 2019, 10 heures 30, École normale supérieure de Lyon Amina Doumane, Cristina Matache Séminaire Chocola http://chocola.ens-lyon.fr/events/ Preuves, programmes et systèmes Jeudi 28 novembre 2019, 10 heures 30, Salle 3052 Valeria Vignudelli (École normale supérieure de Lyon) Bisimulations and trace equivalences for nondeterministic probabilistic systems We study trace-based equivalences for labelled transition systems combining nondeterministic and probabilistic choices. We do so via a coalgebraic construction known as the generalized powerset construction, which consists in first determinizing a system and then recovering trace equivalence as bisimulation equivalence on the determinized system. The generalized powerset construction allows us to apply these two steps, inspired by the standard powerset construction for nondeterministic automata, to a variety of systems, such as labelled transition systems with different computational effects captured by monads (e.g., systems with probabilistic choices). We show how trace semantics for labelled transition systems combining nondeterministic and probabilistic choices can be recovered by instantiating the generalized powerset construction, and we characterise and compare the resulting semantics to known definitions of trace equivalences appearing in the literature. Most of our results are based on the exciting interplay between monads and their presentations via algebraic theories. Preuves, programmes et systèmes Jeudi 21 novembre 2019, 10 heures 30, Salle 3052 Giulio Manzonetto (LIPN and Université Paris Nord) About the power of Taylor expansion The speculative ambition of replacing the old theory of program approximation based on syntactic continuity with the theory of resource consumption based on Taylor expansion and originating from the differential lambda-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in lambda-calculus that are usually demonstrated by exploiting Scott's continuity, Berry's stability or Kahn and Plotkin's sequentiality theory. A paradigmatic example is given by the Perpendicular Lines Lemma for the Böhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity. Preuves, programmes et systèmes Jeudi 14 novembre 2019, 10 heures 30, École normale supérieure de Lyon Francesco Gavazzo, Marie Kerjean, Yann Régis-Gianas Séminaire Chocola http://chocola.ens-lyon.fr/events/ Preuves, programmes et systèmes Jeudi 17 octobre 2019, 10 heures 30, École normale supérieure de Lyon Eric Finster Séminaire Chocola http://chocola.ens-lyon.fr/events/ Preuves, programmes et systèmes Jeudi 3 octobre 2019, 10 heures 30, Salle 3052 Nicolas Behr (IRIF) Stochastic dynamics of graph-like structures In this talk, I will explain the fundamental ideas of stochastic mechanics which led me to investigate the dynamics of graph-like structures, using a new perspective on rewriting systems. My talk is designed to be accessible to a wide audience, and I will thus illustrate my approach on a very simple voter model, expressed in the language of stochastic rewriting. The discussion of this elementary example will clarify the reasons why I am currently working on a general theory of tracelets, mixing ideas from rewriting theory, category theory and concurrency theory, in order to extend the traditional realm of stochastic mechanics, and to implement analysis tools for sophisticated and currently intractable stochastic phenomena on graph-like structures. Preuves, programmes et systèmes Jeudi 26 septembre 2019, 10 heures 30, École normale supérieure de Lyon Pierre Clairambault, Andrea Condoluci, Hugo Férée Séminaire Chocola http://chocola.ens-lyon.fr/events/ Preuves, programmes et systèmes Lundi 2 septembre 2019, 9 heures 30, Amphithéâtre Turing Divers Orateurs Journées PPS 2019 Rencontres de rentrée du pôle PPS de l'IRIF, du lundi 2 au mardi 3 septembre 2019. Accueil à 9h, exposés de 9h30 à 17h30. Programme détaillé disponible sur la page https://www.irif.fr/rencontres/pps2019/index. Preuves, programmes et systèmes Jeudi 20 juin 2019, 10 heures 30, Salle 3052 Alex Simpson (University of Ljubljana) Sheaf principles for reasoning about probabilistic independence Preuves, programmes et systèmes Mercredi 19 juin 2019, 14 heures 30, Salle 3052 Ugo Dal Lago (INRIA and Univ. Bologna) The Geometry of Bayesian Programming We give a geometry of interaction model for a typed lambda-calculus endowed with operators for sampling from a continuous uniform distribution and soft conditioning, namely a paradigmatic calculus for higher-order Bayesian programming. The model is based on the category of measurable spaces and partial measurable functions, and is proved adequate with respect to both a distribution-based and a sampling based operational semantics. Joint work with Naohiko Hoshino Preuves, programmes et systèmes Lundi 17 juin 2019, 11 heures, Salle 3052 Pierre-Malo Deniélou (Google) From MapReduce to Apache Beam: A Journey in Abstraction (This is a joint seminar between the CompSys, PPS, and Verification seminar series.) Processing large amounts of data used to be an affair of specialists: specialized hardware, specialized software, specialized programming model, specialized engineers. MapReduce was the first widely adopted high-level API for large-scale data processing. It helped democratize big data processing by providing a clear abstraction that was supported by several efficient systems. In this talk, I will present how the programming APIs (and underlying systems) for large-scale data processing evolved in the past 20 years, both within Google and in the open source world. I will start from MapReduce and Millwheel and finish with Apache Beam and where we're headed next. Preuves, programmes et systèmes Jeudi 13 juin 2019, 10 heures 30, Salle 3052 Dan Ghica (University of Birmingham, UK) The next 700 abstract machines We propose a new core calculus for programming languages with effects, interpreted using a hypergraph-rewriting abstract machine inspired by the Geometry of Interaction. The intrinsic calculus syntax and semantics only deals with the basic structural aspects of programming languages: variable binding, name binding, and thunking. Everything else, including function abstraction and application, must be provided as extrinsic operations with associated rewrite rules. The graph representation yields natural concepts of locality and robustness for equational properties and reduction rules, which enable a novel flexible and powerful reasoning methodology about (type-free) languages with effects. We illustrate and motivate the technique with challenging examples from the literature. Joint work with Koko Muroya and Todd Waugh Ambridge. Preuves, programmes et systèmes Mardi 11 juin 2019, 11 heures, Salle 3052 Marco Gaboardi (Buffalo University, USA) Differential Privacy: Formal Verification and Applications A vast amount of individuals’ data is collected, stored and accessed every day. These data are valuable for scientific and medical research, for decision making, etc. However, use or release of these data may be restricted by concerns for the privacy of the individuals contributing them. Differential Privacy has been conceived to offer ways to answer statistical queries about sensitive data while providing strong provable privacy guarantees ensuring that the presence or absence of a single individual in the data has a negligible statistical effect on the query's result. In this talk I will introduce differential privacy and present some formal verification techniques we developed to help programmers to certify their programs differentially private and to guarantee that their programs provide accurate answers. These techniques combine approaches based on type systems and program logics with ideas for reasoning about differential privacy using composition, sensitivity and probabilistic coupling. This combination permits fine-grained formal analyses of several basic mechanisms that are fundamental for designing practical differential privacy applications. In addition, I will present some of our results showing how to answer a large number of queries on high dimensional datasets preserving privacy, and how to perform differentially private chi-squared hypothesis testing with the same asymptotic guarantees as the traditional tests. Preuves, programmes et systèmes Jeudi 6 juin 2019, 10 heures 30, Salle 3052 Jean Goubault-Larrecq (ENS Cachan) A Probabilistic and Non-Deterministic Call-by-Push-Value Language There is no known way of giving a domain-theoretic semantics to higher-order probabilistic languages, in such a way that the involved domains are continuous or quasi-continuous - the latter is required to do any serious mathematics. We argue that the problem naturally disappears for languages with two kinds of types, where one kind is interpreted in a Cartesian-closed category of continuous dcpos, and the other is interpreted in a category that is closed under the probabilistic powerdomain functor. Such a setting is provided by Paul B. Levy's call-by-push-value paradigm. Following this insight, we define a call-by-push-value language, with probabilistic choice sitting inside the value types, and where conversion from a value type to a computation type involves demonic non-determinism. We give both a domain-theoretic semantics and an operational semantics for the resulting language, and we show that they are sound and adequate. With the addition of statistical termination testers and parallel if, we show that the language is even fully abstract - and those two primitives are required for that. Preuves, programmes et systèmes Jeudi 16 mai 2019, 10 heures 30, Salle 3052 Lionel Vaux (Amu, Marseille) An application of parallel cut elimination in multiplicative linear logic to the Taylor expansion of proof nets We examine some combinatorial properties of parallel cut elimination in multiplicative linear logic (MLL) proof nets. We show that, provided we impose a constraint on some paths, we can bound the size of all the nets satisfying this constraint and reducing to a fixed resultant net. This result gives a sufficient condition for an infinite weighted sum of nets to reduce into another sum of nets, while keeping coefficients finite. We moreover show that our constraints are stable under reduction. Our approach is motivated by the quantitative semantics of linear logic: many models have been proposed, whose structure reflect the Taylor expansion of multiplicative expo- nential linear logic (MELL) proof nets into infinite sums of differential nets. In order to simulate one cut elimination step in MELL, it is necessary to reduce an arbitrary number of cuts in the differential nets of its Taylor expansion. It turns out our results apply to differential nets, because their cut elimination is essentially multiplicative. We moreover show that the set of differential nets that occur in the Taylor expansion of an MELL net automatically satisfies our constraints. (Joint work with Jules Chouquet.) Preuves, programmes et systèmes Jeudi 2 mai 2019, 10 heures 30, Salle 3052 Hugo Férée (University of Kent) Une théorie de la complexité d'ordre supérieur via la sémantique des jeux Alors que de nombreux modèles de calcul nous permettent de manipuler des données issues de domaines non dénombrables (fonctions d'ordre supérieur, nombres réels, objets définis par co-induction), les différentes notions de complexité ne permettent de s'intéresser qu'à des fonctions d'ordre 1 (i.e. traitant des données finies) voire des fonctions d'ordre 2 (i.e. traitant des fonctions d'ordre 1). Dû à la difficulté de définir une notion pertinente de taille pour des données d'ordre quelconque, les notions de complexité pour des fonctions d'ordre 3 ou plus sont à la fois incomplètes et imparfaites. En nous appuyant sur la sémantique des jeux nous proposons ici une définition de taille et de complexité pour les fonctions d'ordre supérieur de PCF, et plus généralement pour tout processus calculatoire assimilable à une certaine classe de jeux séquentiels. Preuves, programmes et systèmes Mardi 2 avril 2019, 10 heures 30, Salle 3052 Jérémy Dubut (NII, Tokyo) Categorical approaches to bisimilarity There are different categorical approaches to variations of transition systems and their bisimulations. One is coalgebras, another one is open maps. In this talk, I will describe these two approaches, illustrated by the case of labelled transition systems (almost no knowledge in category theory is needed for this part). I will then describe how it is possible to translate one into the other in some cases. From open maps to coalgebras, this was done by Lasota, using multi-sorted transition systems. From coalgebras to open maps, this was done in my joint work with Thorsten Wißmann, Shin-ya Katsumata and Ichiro Hasuo, where we derived path-categories and trace semantics for free for different flavors of categories of coalgebras with non-deterministic branching. I will illustrate those constructions on various concrete examples (tree automata, regular nominal automata, …). Preuves, programmes et systèmes Jeudi 28 mars 2019, 10 heures 30, Salle 3052 Thomas Leventis (Univ. Bologna (Italy)) Taylor expansion of probabilistic lambda-terms Taylor expansions have been introduced by Ehrhard and Regnier as a computational interpretation of Girard's quantitative semantics. Lambda-terms are expanded into linear combinations of their n-linear approximants, such approximants being defined as resource lambda-terms. This construction is well-suited to interpret quantitative calculi, such as the probabilistic lambda-calculus: Taylor expansions are linear combinations and the resource lambda-calculus is linear so interpreting probability distributions over terms is straightforward. Yet paradoxically the proof technique used by Ehrhard and Regnier to study Taylor expansions heavily rely on the particular structure of the expansions of ordinary lambda terms, and they are not suited to work on a quantitative setting. In this talk we will show how to indirectly extend their result to probabilistic Taylor expansions. First we will introduce explicit Taylor expansions, which uses “inert” probabilistic choices to interpret probabilistic terms while preserving the necessary properties to apply Ehrhard and Regnier's proof techniques. Then we will show how to extract interesting results on probabilistic Taylor expansions from these explicit Taylor expansions. Preuves, programmes et systèmes Jeudi 21 mars 2019, 10 heures 30, Salle 3052 Paolo Pistone (Univ. Tubingen) Quelques résultats sur l'équivalence des preuves dans la logique linéaire du second ordre Les réseaux de preuves donnent une représentation canonique des démonstrations dans la logique linéaire multiplicative : l'équivalence dénotationnelle des preuves coïncide avec l'équivalence des réseaux. Par contre, la canonicité des réseaux ne s'étend pas au second ordre. Ce problème est du à la présence des témoins des règles existentielles. En fait, dans plusieurs sémantiques dénotationnelles l'information portée par les preuves est compressée, et notamment les témoins existentiels sont effacés. Font partie de ces sémantiques “effaçantes” les sémantiques cohérente et rélationnelle, ainsi que la sémantique dinaturelle et la sémantique observationnelle. On présente des résultats sur l'équivalence des preuves dans ces sémantiques et on discute des applications en complexité dues à la possibilité de compresser les preuves. Une partie de ces travaux est issue d'une collaboration avec L. Tortora de Falco, T. Seiller et L.T.D. Nguyễn. Preuves, programmes et systèmes Jeudi 28 février 2019, 10 heures 30, Salle 3052 François Bergeron (UQAM) Theory of species of structures and applications Species of Structures, introduced almost 40 years ago, give a natural conceptu l framework for the notion of ``combinatorial construction on sets’’. Fundamental operations between species allow the specification of new species in terms of known ones, giving a systematic context for the solution of classical enumeration questions, including both labelled and unlabelled enumeration (a.k.a. Pólya Theory). In this talk, we will give an accessible introduction to the Theory of Species, with many illustrations. If time allows, we will also survey some of many areas (computer science, theoretical physics, chemistry, etc.) where they are currently useful. Preuves, programmes et systèmes Mardi 26 février 2019, 10 heures 30, Salle 3052 Eric Finster (Inria - Nantes) Higher Universal Algebra in Dependent Type Theory The naive translation of set-theoretic definitions of algebraic structures (such as monoids, categories and groups) into Martin-Lof type theory is often incomplete: without additional hypotheses such as truncation or a decidable equality, these translations fail to specify the behavior of the structure with respect to higher equalities. On the other hand, a complete description of such structures is quite difficult, as it typically requires the specification of an infinite number of equations. I will present recent progress on this problem by giving a definition of a “coherent polynomial monad” internal to type theory. Preuves, programmes et systèmes Jeudi 21 février 2019, 10 heures 30, Salle 3052 Damiano Mazza (CNRS) Intersection Types and Runtime Errors in the Pi-Calculus We introduce a type system for the $\pi$-calculus which is designed to guarantee that typable processes are well-behaved, namely they never produce a run-time error and, even if they may diverge, there is always a chance for them to “finish their work”, i.e. to reduce to an idle process. The introduced type system is based on non-idempotent intersections, and is thus very powerful as for the class of processes it can capture. Indeed, despite the fact that the underlying property is $\Pi^0_2$-complete, there is a way to show that the system is complete, i.e., that any well-behaved process is typable, although for obvious reasons infinitely many derivations need to be considered. Joint work with Ugo Dal Lago, Marc De Visme, Akira Yoshimizu Preuves, programmes et systèmes Jeudi 7 février 2019, 10 heures 30, Salle 3052 Sandra Alves Linearisation of the lambda-calculus and its termination The notion of linearisation of the lambda-calculus has been explored in different settings: Damas and Florido used information given by intersection types, to define a notion of expansion of terms in the lambda-calculus into linear terms; Kfoury embedded the lambda-calculus into a new linear calculus, with a new notion of “linear” reduction, and linearization was defined indirectly by means of a notion of contraction of expanded terms in the new calculus into standard lambda-terms; Alves and Florido defined a notion of linearisation from standard lambda-terms into a linear subset, called the weak linear lambda-calculus, by using the notion of computation as paths, deriving from Lévy’s labelled lambda-calculus. In this talk we will explore these previous works, discuss their relation and present some open problems regarding the termination of linearisation methods. Preuves, programmes et systèmes Jeudi 24 janvier 2019, 10 heures 30, Ens Lyon Seminaire Chocola (Ens Lyon) Non encore annoncé. Preuves, programmes et systèmes Jeudi 10 janvier 2019, 10 heures 30, Salle 3052 Aurore Alcolei (Ens Lyon) Concurrent strategies for Herbrand's theorem Herbrand's theorem exposes some of the constructive content of classical logic. In its simplest form, it reduces the validity of a first-order purely existential formula to that of a finite disjunction. More generally, it reduces first-order validity to propositional validity, by understanding the structure of the assignment of first-order terms to existential quantifiers, and the causal dependency between quantifiers. In this talk, we show that Herbrand's theorem in its general form can be elegantly stated and proved as a theorem in the framework of concurrent games, a denotational semantics designed to faithfully represent causality and independence in concurrent systems. Closely related to expansion trees, the causal structure of concurrent strategies, paired with annotations by first-order terms, is used to specify the dependency between quantifiers. As furthermore these strategies can be composed we are able to interpret classical sequent proofs, yielding a compositional proof of Herbrand's theorem.