Rencontre, 9 février 2017

Programme

10:30 – 12:00

Danko Ilic

Invited talk: Exp-log 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 meta-theoretic 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 first-order quantifiers and define a constructive arithmetical hierarchy of formulas resembling the classical arithmetical hierarchy.

http://hal.inria.fr/hal-00991147

http://arxiv.org/abs/1502.04634

http://arxiv.org/abs/1601.04876

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 fully-abstract compiler guarantees that the semantics of the low-level target language does not leak into source programs.

Abstraction leaks are also usability issues. Multi-language 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 multi-language 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 multi-language 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 Dezani-Ciancaglini 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 proof-theoretical point of view. We give a sequent calculus presentation IS of BCD subtyping and study its core properties: cut-elimination, sub-formula 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.

• slides