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 10 mars, 10h30

                               ---------------
                               Gabriel Scherer
                               ---------------

                                    INRIA

         ===========================================================
         Maximal multi-focusing for sum equivalence: an introduction
         ===========================================================

In this talk, I hope to give a self-contained presentation of
((maximal) multi-)focusing. Focusing is a major technique in proof
search since the nineties; it removes some redundancy in sequent or
natural deduction proofs, and had a deep impact on logic programming.
Multi-focusing [1] is a relatively recent generalization which
provides a very strong but hard-to-compute notion of canonicity. If
time allows, I'll sketch the relation between maximal multi-focused
proofs (as in [2]) and an existing rewriting algorithm [3] that
computes beta-eta-equivalence of programs in the simply-typed
lambda-calculus with sums.

[1] From proofs to focused proofs: a modular proof of focalization in
linear logic
Dale Miller, Alexis Saurin (2007)
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.95.4424

[2] Canonical Sequent Proofs via Multi-Focusing
Kaustuv Chaudhuri, Dale Miller, Alexis Saurin (2008)
http://www.pps.univ-paris-diderot.fr/~saurin/Publi/multifoc.pdf

[3] Extensional rewriting with sums
Sam Lindley (2007)
http://homepages.inf.ed.ac.uk/slindley/papers/sum.pdf