Salidou day, 15 novembre 2018
This meeting will take place in Paris. We will celebrate the addition of new members to the Chocola gang, from Nantes: the Gallinette research team.
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
Programme
- 11:00 – 12:30
-
Éric Tanter (Universidad de Chile & Inria Paris)
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)
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 lack 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
This is not part of the CHoCoLa day, but you might be interested in attending! See this page.
