Séminaire, 5 novembre 2015

Programme

10:30 – 12:00

Bob Atkey (Strathclyde Univ., UK)

Invited talk: Type systems for programming with coinductive data types

(title to be confirmed)

14:00 – 15:00

Gabriel Scherer (INRIA)

Invited talk: Multi-focusing the lambda-calculus.

In this talk, I would like to present applications of maximal multi-focusing to programming languages problems -- in the simply-typed lambda-calculus with both negative types (such has functions) and positive types (such as sums). Focusing seems to be a key ingredient in extending existing intuitions on beta-eta equivalence from the purely negative fragment (functions and pairs) to a more diverse system with types of both polarities. I will present focusing and multi-focusing (for propositional intuitionistic logic, that is the simply-typed lambda-calculus), and its use to enumerate canonical inhabitants of a type (in particular testing whether a type has a unique inhabitant) and to test typed program equivalence (even in presence of the empty type).

15:30 – 16:30

Jean-Jacques Lévy (INRIA)

Invited talk: The cost of usage in the lambda-calculus