http://chocola.ens-lyon.fr/events/meeting-2018-12-13/

Implicative Algebras were recently introduced as a unified framework for forcing and realisability, whose particularity is to interpret terms and formulæ uniformly.

In this ongoing work with Alexandre Miquel, we show how linear logic fits in this picture: we present a family of models, where certain computational principles are distinguished, and argue thata it provides a satisfactory meaning explanation of the connectives of (perfective) linear logic.

In this talk I will review G4ip, a simple calculus for intuitionistic propositional logic (IPL) that provides a decision procedure for provability. Its basic mechanisms can be traced back to Vorob'ev in the 50s, and were found again by Hudelmaier (88), Dyckhoff (90), Paulson (91), and (with a linear logic flavour) Lincoln-Scedrov-Shankar (91). In 2015, Claessen and Rosén presented the fastest decision procedure for IPL, based on SMT-solving techniques. We describe their algorithm and show how it can be seen as a variant of the aforementioned calculus, albeit with key variations that provide increased performance. Their algorithm relies on a SAT-solver used as a black box and treats intuitionistic entailment as a theory. We show how the recent framework of model-constructing satisfiability for SMT-solving could further integrate intuitionistic reasoning within the main SAT-solving loop. This would constitute an intuitionistic variant of the main algorithm of SAT-solvers, where Kripke models are built instead of Boolean models.

11:00 – 12:30 Éric Tanter (Universidad de Chile & Inria Paris) - Invited talk: Abstracting Gradual Typing: Principles and Application to Gradual Parametricity

  Gradual typing enables programming languages to seamlessly combine dynamic and static checking. Language researchers and designers have extended a wide variety of type systems to support gradual typing. These efforts consistently demonstrate that designing a satisfactory gradual counterpart to a static type system is challenging, and this challenge only increases with the sophistication of the type system. Gradual type system designers need more formal tools to help them conceptualize, structure, and evaluate their designs. Based on an understanding of gradual types as abstractions of static types, we have developed systematic foundations for gradual typing based on abstract interpretation, called Abstracting Gradual Typing (AGT for short). Gradual languages designed with the AGT approach satisfy, by construction, the established criteria for gradually-typed languages. In this talk, I will give a brief introduction to AGT in a simply-typed setting, and will then discuss recent work on a gradual counterpart of System F that enforces relational parametricity, even in the presence of imprecise types.

14:00 – 15:00 Flavien Breuvart (Université Paris 13) - Invited talk: Graded Types Parametricity : Principles and Application to Abstract Interpretation

  In this talk, we will briefly present the yet-to-start project CoGITARe, which aims at developing further graded types expressivity and inference in order to use them to perform abstract interpretations.
  In a second time, we give an historic on graded type systems and their expressivity. Then, we will see that this expressivity is limited by a lake of dependency/parametricity. We will thus explore two ongoing research directions that adds two very different kind of parametricity to graded types.
  (The provocative title should only be taken as a joke. Despite their apparent similitudes, this work and Éric Tanter's have vastly different objectives and involved different issues and techniques. In particular, notice that gradual and graded types are fundamentally different.)

15:30 – 16:30 Shane Mansfield (Univ. of Oxford) - Invited talk: An overview of empirical models

  Empirical models are a way of formalising data that arises in physical experiments. They were first proposed by Abramsky and Brandenburger as part of a framework to analyse fundamentally non-classical phenomena in quantum systems. Conveniently from a computer science perspective, they abstract away from the mathematical baggage of quantum theory and instead allow the key phenomena to be characterised purely as features of empirical data. After introducing the basic framework I will discuss some more recent results and developments, drawing on joint work with a number of collaborators. In particular: quantum computations can simply be modelled as classical computations with the additional ability to interact with a resource empirical model; quantitative measures of non-classicality can be shown to relate directly to some basic quantum-over-classical computational advantages; and the beginnings of a category-theoretic approach to reasoning about empirical models have emerged.

18:00 – 19:00 Xavier Leroy - Lecture: Leçon inaugurale au Collège de France

  This is not part of the CHoCoLa day, but you might be interested in attending! See https://www.college-de-france.fr/site/xavier-leroy/inaugural-lecture-2018-11-15-18h00.htm

  The meeting will take place in Bâtiment Sophie Germain, here.
  We will first gather at the 3rd floor of the building, for a breakfast.
  We will then move for the talk of the morning (11.00-12.30) to Amphi Turing.
  We will have lunch in room 3052
  In the afternoon (14h-16h30), we will be in room 1016

Journées PPS 2018

Journées PPS 2018

We propose a type-based analysis to infer the session protocols of channels in an ML-like concurrent functional language. Combining and extending well-known techniques, we develop a type-checking system that separates the underlying ML type system from the typing of sessions. Without using linearity, our system guarantees communication safety and partial lock freedom. It also supports provably complete session inference with no programmer annotations. We exhibit the usefulness of our system with interesting examples, including one which is not typable in substructural type systems.

Guarded recursion has emerged as a natural paradigm for programming with infinite data structures in type theory and high-assurance functional languages. In the first part of this talk, I will present some intuitions behind guarded recursion, using programming examples. In a second part, I will discuss ongoing work on a typed lambda-calculus equipped with rich facilities for defining and manipulating guarded recursive types.

(joint work with J. Weinberger)

Abstract: Voevodsky's model of the Univalence Axion in simplicial sets is not constructive as shown by Coquand et al. To avoid this problem Cohen, Coquand, Huber, Moertberg have constructed in Cubical Sets a model of a Cubical Type Theory which has computational meaning.

We show that simplicial sets form a subtopos of cubical sets which allows one to contructively reason in the latter about the former.

I will give a new definition of partial Higher Dimension Automata – a geometric model for true concurrency – using lax functors. This definition is simpler than the original, and more natural from a categorical point of view, but also matches more clearly the intuition that pHDA are Higher Dimensional Automata with some missing faces. I will then focus on trees. Originally, for example in transition systems, trees are defined as those systems that have a unique path property. To understand what kind of unique path property is needed in pHDA, I will start by looking at trees as colimits of paths. From this, I will deduce that trees are exactly the pHDA with the unique path property modulo a notion of homotopy, and without any shortcuts. This property will allow me to prove two interesting characterisations of trees: trees are exactly those pHDA that are the unfolding of another pHDA; trees are exactly the cofibrant objects, much as in the language of Quillen’s model structures. In particular, this last characterisation gives the premisses of a new understanding of concurrency theory using homotopy theory.

In a 2012 paper, Richard Statman exhibited an inference system, based on second order monadic logic and non-terminating rewrite rules, that exactly types all strongly normalizable lambda-terms. We show that this system can be simplified to first-order minimal logic with rewrite rules, along the Deduction Modulo Theory lines.

We show that our rewrite system is terminating and that the conversion rule respects weak versions of invertibility of the arrow and of quantifiers. This requires additional care, in particular in the treatment of the latter. Then we study proof reduction, and show that every typable proof term is strongly normalizable and vice-versa.

On discutera différentes manières de relier syntaxiquement la logique linéaire classique (LL) et sa version intuitionniste (ILL) : d'une part à travers la question de la conservativité de LL sur ILL (contre-exemples et conditions suffisantes), et d'autre part via l'étude de non-non traductions de LL dans ILL. On montrera que ces traductions permettent de représenter des extensions de LL dans ILL, mais aussi qu'elles peuvent être utilisées comme outil pour prouver des propriétés de LL : élimination des coupures et focalisation par exemple. Ces différents résultats ont été formalisés en Coq à l'aide de la bibliothèque Yalla, que nous présenterons brièvement.

There exists a large spectrum of techniques for proving correctness of computer programs. At one end is the Curry-Howard isomorphism, in which a typing procedure automatically checks the correctness of a program, and at the other end are techniques à la Hoare, in which non-trivial reasonning is performed in a logic adapted to the programming language. Realizability can be seen as a mixture of these two approaches: proving that a program realizes a specification is done via a combination of automatic techniques in a Curry-Howard fashion, and manual proofs of correctness of subprograms with respect to some axioms. In my talk I will present some realizability models where the realizability relation is defined semantically: a program realizes a specification if its denotation satisfies a property in the model. The denotational models involved include game semantics, continuation models and Scott domains.

This talk will present SyTeCi, the first general automated tool to check contextual equivalence for programs written in a typed higher-order language with references (i.e. local mutable states), corresponding to a fragment of OCaml.

After introducing the notion of contextual equivalence, we will see on some examples why it is hard to prove such equivalences (reentrant calls, private states). As we will see, such examples can be found in many different programming languages.

Then, we will introduce SyTeCi, a tool to automatically check such equivalences. This tool is based on a reduction of the problem of contextual equivalence of two programs to the problem of reachability of “error states” in transition systems of memory configurations.

Contextual equivalence being undecidable (even in a finitary setting), so does the non-reachability problem for such transition systems. However, one can apply model-checking techniques (predicate abstraction, summarization of pushdown systems) to check non-reachability via some approximations. This allows us to prove automatically many non-trivial examples of the literature, that could only be proved by hand before. We will end this talk by the presentation of a prototype implementing this work.

No one is without knowing the famous Shadok principle « the more it fails, the more likely it will eventually succeed. » Taking inspiration from this unfathomable wisdom, we came up with a dependent type theory which allows failure, so that we could succeed more in proving things. Such a Shadok theory is justified by translating it away into vanilla dependent theory, just as a mundane compiler would, where failing can be interpreted as a call-by-name exception mechanism. En passant, this gives the first full syntactical model of the Calculus of Inductive Constructions introducing effects.

Alas! The right to fail succeeds a tad too much, insofar as the resulting Shadock type theory is logically inconsistent. Not being impressed in any way, we put order into this madness by requiring that no exception should ever reach toplevel, thanks to a clever use of a variant of Bernardy-Lasson syntactic parametricity. While the former model can be thought of as Friedman A-translation applied to CIC, the latter is no more than a principled variant of Kreisel's modified realizability that scales to dependent types. In particular, it readily gives a model of CIC that still has canonicity, strong normalization and decidable type-checking, while featuring new principles typical of modified realizability such as the independence of premises and unprovability of Markov's principle.

https://www.pédrot.fr/articles/exceptional.pdf

The causal structure of spacetime defines a (pair of) natural order structures on the underlying set of events. Much of the analysis of cauasl structure involves a delicate interplay between order, topology and geometry. In view of the fundamental role of the causal order in certain approaches to quantum gravity as well as its fundamental role in concurrency theory one can ask whether the topology can be derived from pure order theoretic considerations.

In a remarkable example of serendipity, order theory has been developed by computer scientists and mathematicians in order to capture computability concepts. Dana Scott developed a notion of a continuous lattice or continuous poset with a view to capturing computability as continuity with a suitable topology that has come to be known as the Scott topology. This subject has acquired the name of ``domain theory.''

We applied domain theory to the problem of reconstructing the spacetime topology from the order and came up with a number of results about reconstruction of spacetime structure from just a countable dense set.

We prove that a globally hyperbolic spacetime with its causality relation is a bicontinuous poset whose interval topology is the manifold topology. From this one can show that from only a countable dense set of events and the causality relation, it is possible to reconstruct a globally hyperbolic spacetime in a purely order theoretic manner. The ultimate reason for this is that globally hyperbolic spacetimes belong to a category that is equivalent to a special category of domains called interval domains.

This was joint work with Keye Martin of Naval Research Laboratories.

Software-based countermeasures provide effective mitigation against side-channel attacks, often with minimal efficiency and deployment overheads. Their effectiveness is often amenable to rigorous analysis: specifically, several popular countermeasures can be formalized as information flow policies, and correct implementation of the countermeasures can be verified with state-of-the-art analysis and verification techniques. However, in absence of further justification, the guarantees only hold for the language (source, target, or intermediate representation) on which the analysis is performed.

We consider the problem of preserving side-channel countermeasures by compilation for cryptographic “constant-time”, a popular countermeasure against cache-based timing attacks. We present a general method, based on the notion of 2-simulation, for proving that a compilation pass preserves the constant-time countermeasure. Using the Coq proof assistant, we verify the correctness of our method and of several representative instantiations.

http://chocola.ens-lyon.fr/events/meeting-2018-02-08

10:30 – 12:00

  Prakash Panangaden (Mc Gill University, Canada)
  Quantitative Equational Logic 

14:00 – 15:00

  Justin Hsu (University College London, UK)
  From Couplings to Probabilistic Relational Program Logics 

15:30 – 16:30

  Thomas Ehrhard (IRIF, Univ. Paris Diderot)
  Stable and measurable functions on positive cones: a model of probabilistic functional languages with continuous types

Many program properties are relational, comparing the behavior of a program (or even two different programs) on two different inputs. While researchers have developed various techniques for verifying such properties for standard, deterministic programs, relational properties for probabilistic programs have been more challenging. In this talk, I will survey recent developments targeting a range of probabilistic relational properties, with motivations from privacy, cryptography, machine learning. The key idea is to meld relational program logics with an idea from probability theory, called a probabilistic coupling. The logics allow a highly compositional and surprisingly general style of analysis, supporting clean proofs for a broad array of probabilistic relational properties.

Bio: Justin Hsu is a post-doctoral researcher at the University College of London. He obtained his graduate degree from the University of Pennsylvania. His research interests span formal verification and theoretical computer science, including verification of randomized algorithms, differential privacy, and game theory.