Vous pouvez vous abonner à nos annonces de séminaires
http://gallium.inria.fr/seminaires/
S E M I N A I R E
__
/ _` _ / / o
/ ) __) / / / / / /\/|
(___/ (_/ (_ (_ / (__/ / |
I N R I A - Rocquencourt
Amphi Turing du bâtiment 1
Lundi 30 mars, 10h30
---------------
Gabriel Scherer
---------------
INRIA
============================================
Which simple types have a unique inhabitant?
============================================
In this talk I will present an algorithm that takes a type of the simply-typed
lambda-calculus with sums, and says that:
(0) it is not inhabited, or
(1) it is uniquely inhabited (and gives the unique program at this type), or
(2) it is not uniquely inhabited (and gives two distinct programs at this type).
The algorithm relies on a novel "saturating" variant of focused intuitionistic
logic, which is very close to the existing notion of maximal multi-focusing.
Its termination uses techniques of propositional proof search, that needed to
be adapted to preserve computational correctness: if you cut the search space
too harshly, you may claim a type is uniquely inhabited when it is not.
P.S.: I will also give this talk in PPS on April 1st.