Séminaire, Nov. 5, 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: Multifocusing the lambdacalculus.
In this talk, I would like to present applications of maximal multifocusing to programming languages problems  in the simplytyped lambdacalculus 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 betaeta equivalence from the purely negative fragment (functions and pairs) to a more diverse system with types of both polarities. I will present focusing and multifocusing (for propositional intuitionistic logic, that is the simplytyped lambdacalculus), 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

JeanJacques Lévy (INRIA)Invited talk: The cost of usage in the lambdacalculus