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