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.