Rencontre, Feb. 9, 2017
La rencontre aura lieu à l'ENS de Lyon, site Monod, en amphi B (3ème étage).
Programme
 10:30 – 12:00

Invited talk: Explog normal form of types and formulas
In this lecture, we will look at the decomposition of the arrow type (i.e. intuitionistic implication) in terms of unary exponentiation and logarithm, and show some applications of it.
We will start by recalling the notion of type isomorphism, reviewing the metatheoretic facts that hold of it in presence of disjoint union types.
We shall then show that it makes sense to use the transformation aᵇ=exp(b·log(a)) in the context of types by defining a normal form for the type language {→,×,+} and applying it to obtain a simplification of the standard axioms of ηequality for the {→,×,+}typed λcalculus.
We shall end by hinting at proof theoretic applications. In particular, we shall show how to extend the type normal form to the firstorder quantifiers and define a constructive arithmetical hierarchy of formulas resembling the classical arithmetical hierarchy.
http://hal.inria.fr/hal00991147
 14:00 – 15:00

Gabriel Scherer (Northeastern University, Boston)Invited talk: Full abstraction for language design
A transformation between languages is fully abstract if it preserves observational equivalence. Full abstraction has been proposed as a desirable formal property of compilers: a fullyabstract compiler guarantees that the semantics of the lowlevel target language does not leak into source programs.
Abstraction leaks are also usability issues. Multilanguage programming systems are widely used, but often exhibit unfortunate, unplanned interactions. We propose to use full abstraction for language design: if the embedding of a single language into the multilanguage system is fully abstract, we know that it interacts gracefully with the other languages of the system.
We demonstrate our approach by a case study, of a proposed multilanguage design that combines a simple ML language with a linear language with linear mutable state. We prove that programmers knowing only the ML side of the story will not have bad surprises when interacting with code that may, internally, use the linear language.
 15:30 – 16:30

Olivier Laurent (CNRS, ENS de Lyon)Invited talk: On the Proof Theory of BCD Intersection Subtyping
In their 1983 paper, Barendregt, Coppo and DezaniCiancaglini defined an intersection type system, now known under the name BCD. This system relies on a subtyping relation, and most of the properties of BCD typing are related with properties of BCD subtyping. We thus focus on the study of BCD subtyping.
By understanding the BCD subtyping relation as a deduction relation, we propose to look at it from a prooftheoretical point of view. We give a sequent calculus presentation IS of BCD subtyping and study its core properties: cutelimination, subformula property, rule inversions, beta condition, etc. Thanks to a Girard's style translation of IS, we prove that BCD subtyping can be seen as a fragment of Lambek's calculus. Finally we address ongoing work on the computational complexity of BCD subtyping, as well as alternative presentations and possible extensions.