~~NOCACHE~~
/* DO NOT EDIT THIS FILE             */

[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 13 décembre 2018, 10 heures 30, ENS Lyon\\
**Journée Chocola**  //ENS Lyon//
<button type="link" size="xs" collapse="b4-773">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b4-773" collapsed="true">
<well size="sm">
http://chocola.ens-lyon.fr/events/meeting-2018-12-13/
</well>
</collapse>


[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 6 décembre 2018, 10 heures 30, Salle 3052\\
**Luc Pellissier** (IRIF) //Linear Implicative Algebras, towards a Brouwer-Heyting-Kolmogorov interpretation of linear logic//
<button type="link" size="xs" collapse="b4-774">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b4-774" collapsed="true">
<well size="sm">
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.
</well>
</collapse>


[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 22 novembre 2018, 10 heures 30, Salle 3052\\
**Stéphane Graham-Lengrand** (LIX, CNRS) //The intuitionistic calculus that was discovered 6 times//
<button type="link" size="xs" collapse="b4-775">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b4-775" collapsed="true">
<well size="sm">
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.
</well>
</collapse>


[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 15 novembre 2018, 11 heures, Salle 3052 + Amphi Turing + 1016\\
**Eric Tanter, Flavien Breuvart, Shane Mansfield & Xavier Leroy** (Chocola meeting in Paris) //Salidou's day//
<button type="link" size="xs" collapse="b4-776">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b4-776" collapsed="true">
<well size="sm">
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
</well>
</collapse>


[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Vendredi 9 novembre 2018, 9 heures 30, Salle 3052\\
**Pôle Preuves, Programmes Et Systèmes**  //Journées 2018//
<button type="link" size="xs" collapse="b4-777">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b4-777" collapsed="true">
<well size="sm">
[[::rencontres:pps2018:]]
</well>
</collapse>


[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 8 novembre 2018, 9 heures 30, Salle 3052\\
**Pôle Preuves, Programmes Et Systèmes**  //Journées 2018//
<button type="link" size="xs" collapse="b4-778">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b4-778" collapsed="true">
<well size="sm">
[[::rencontres:pps2018:]]
</well>
</collapse>


[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 25 octobre 2018, 10 heures 30, Salle 3052\\
**Carlo Spaccasassi** (Microsoft Research Cambridge, Cambridge (United Kingdom)) //Type-Based Analysis for Session Inference//
<button type="link" size="xs" collapse="b4-779">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b4-779" collapsed="true">
<well size="sm">
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.
</well>
</collapse>


[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 4 octobre 2018, 10 heures 30, Salle 3052\\
**Adrien Guatto** (IRIF) //Towards A General Guarded Lambda-Calculus//
<button type="link" size="xs" collapse="b4-780">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b4-780" collapsed="true">
<well size="sm">
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.
</well>
</collapse>


[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 27 septembre 2018, 10 heures 30, Salle 3052\\
**Thomas Streicher** (TU Darmstadt) //Simplicial sets inside cubical sets//
<button type="link" size="xs" collapse="b4-781">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b4-781" collapsed="true">
<well size="sm">
(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.
</well>
</collapse>


[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 5 juillet 2018, 10 heures 45, Salle 3052\\
**Jeremy Dubut** (National Institute of Informatics Tokyo, Japan) //Higher-Dimensional Automata//
<button type="link" size="xs" collapse="b4-782">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b4-782" collapsed="true">
<well size="sm">
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.
</well>
</collapse>


[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 28 juin 2018, 10 heures 30, Salle 3052\\
**Olivier Hermant** (CRI, Mines ParisTech) //Intersection Types in Deduction Modulo Theory//
<button type="link" size="xs" collapse="b4-783">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b4-783" collapsed="true">
<well size="sm">
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.
</well>
</collapse>


[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 31 mai 2018, 10 heures 30, Salle 3052\\
**Olivier Laurent** (ENS Lyon) //Balade entre logiques linéaires classiques et intuitionnistes//
<button type="link" size="xs" collapse="b4-784">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b4-784" collapsed="true">
<well size="sm">
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.
</well>
</collapse>


[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 29 mars 2018, 14 heures, Salle 3052\\
**Valentin Blot** (LRI) //Realizability: denotational semantics for correctness//
<button type="link" size="xs" collapse="b4-785">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b4-785" collapsed="true">
<well size="sm">
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.
</well>
</collapse>


[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 29 mars 2018, 10 heures 30, Salle 3052\\
**Guilhem Jaber** (LIP) //Model-checking contextual equivalence of higher-order programs with references.//
<button type="link" size="xs" collapse="b4-786">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b4-786" collapsed="true">
<well size="sm">
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.
</well>
</collapse>


[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 22 février 2018, 10 heures 30, Salle 3052\\
**Pierre-Marie Pédrot** (Max Planck Institute for Software Systems, Saarbrücken, Germany) //Failure is Not an Option, or The Curry-Howard-Shadok correspondence//
<button type="link" size="xs" collapse="b4-787">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b4-787" collapsed="true">
<well size="sm">
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
</well>
</collapse>


[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 15 février 2018, 10 heures 30, Salle 3052\\
**Prakash Panangaden** (McGill University) //Topology, Order and Causal Structure//
<button type="link" size="xs" collapse="b4-788">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b4-788" collapsed="true">
<well size="sm">
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.
</well>
</collapse>


[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 8 février 2018, 10 heures 30, Salle 3052\\
**Vincent Laporte** (IMDEA Software) //Provably secure compilation of side-channel countermeasures: the case of cryptographic "constant-time"//
<button type="link" size="xs" collapse="b4-789">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b4-789" collapsed="true">
<well size="sm">
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.
</well>
</collapse>
Joint session Verification/PPS

[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 8 février 2018, 10 heures 30, Salle 3052\\
**Séminaire Chocola** (ENS Lyon) //Rencontres Chocola de Février: Prakash Panangaden, Justin Hsu & Thomas Ehrhard//
<button type="link" size="xs" collapse="b4-790">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b4-790" collapsed="true">
<well size="sm">
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
</well>
</collapse>


[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 25 janvier 2018, 10 heures 30, Salle 3052\\
**Justin Hsu** (University College of London) //From Couplings to Probabilistic Relational Program Logics//
<button type="link" size="xs" collapse="b4-791">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b4-791" collapsed="true">
<well size="sm">
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.
</well>
</collapse>