Séminaire, Nov. 5, 2015

Programme

10:30 – 12:00
Bob Atkey (Strathclyde Univ., UK)

(title to be confirmed)

14:00 – 15:00
Gabriel Scherer (INRIA)

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