Institut de Mathématiques de Luminy

SÉMINAIRES 2013
Logique et Interactions

Organisateur :
Emmanuel Beffara (tél. 04 91 26 96 35)
Lieu : IML, Bâtiment TPR2- CNRS :
Salle de Séminaires : 3ème étage (304-306).
Horaire : en règle générale le jeudi, à 14h.


jeudi 10 octobre

à 14h
Lionel Rieg

Lionel Rieg
(LIP, ENS Lyon) :
L'interprétation calculatoire du forcing en réalisabilité classique : l'exemple des arbres de Herbrand

Webpage : http://perso.ens-lyon.fr/lionel.rieg/

Résumé : Jean-Louis Krivine a présenté en 2011 une méthode pour combiner le forcing de Cohen et la réalisabilité classique dans laquelle les conditions de forcing s'interprètent calculatoirement comme des références non soumises aux backtracks. Alexandre Miquel a reformulé la traduction de programme sous-jacente dans un cadre typé, l'arithmétique d'ordre supérieur (PAω⁺) et l'a intégré directement à la KAM, donnant la KFAM (Krivine's Forcing Abstract Machine).
Dans cet exposé, je vais donner les idées essentielles de cette transformation de programme issue du forcing et expliquer comment elle peut s'utiliser en pratique. J'illustrerai ensuite cette méthodologie par un exemple concret : la construction d'arbre de Herbrand.


vendredi 20 septembre

à 10h
Michele Basaldella

Michele Basaldella
(IML, Marseille) :
An interactive semantics for classical arithmethic

Webpage : http://www.kurims.kyoto-u.ac.jp/~mbasalde/

Abstract: In this talk, we present a semantics of derivations for an infinitary logic introduced by Novikoff and later refined by Coquand and Herbelin. The language of this logic consists of infinitary propositional formulas, and the proof-system for this language is given by a sequent calculus with infinitary rules of inferences.
First-order classical arithmetic can be naturally embedded in this logic. The semantics of derivations we develop in this paper is strongly inspired by Girard’s ludics. The main result of this paper is a soundness-and-completeness theorem for derivations in the infinitary logic with respect to this kind of semantics.

à 14h
Clément Aubert

Clément Aubert
(IML, Marseille) :
Proof circuits and parallel cut-elimination
in logarithmic space

Webpage : http://lipn.univ-paris13.fr/~aubert/

Abstract: Terui, Mogbil and Rahli detailed how it was possible to compute Boolean functions in parallel with proof-nets for MLLu. We introduced Proof circuits to lighten the encoding of Boolean Circuits into proof-nets, extending previous results to sub-logarithmic classes of complexity. It happened that this way of constraining our proof-nets eased their simulation by Alternating Turing Machine, the most general kind of Turing Machine. We present a small extension to previous results, where proof-nets can be normalized with logarithmic space.


Logo LIF

jeudi 23 mai
Amphi 12 (Bâtiment B)
Jérôme Fortier
(LIF, Marseille)
Règles de coupure dans les preuves circulaires

Webpage : http://www.lif.univ-mrs.fr/

Résumé : Les preuves circulaires, dans lesquelles certaines conclusions peuvent être démontrées à partir d'elles-mêmes, furent introduites dans [1] pour étudier la calculabilité dans les modèles du μ-calcul, soit avec les opérations suivantes: produits et coproduits finis, algèbres initiales et coalgèbres terminales. Le calcul en question, sans règle de coupure, était correct et complet, mais pas plein, c'est-à-dire qu'il ne représentait pas toute la structure des modèles catégoriques visés.
On remplit donc le système de preuves circulaires en introduisant la règle de coupure. La nouvelle syntaxe permet une procédure d'élimination des coupures qui produit un arbre infini, modélisant ainsi le calcul recherché.
Plusieurs directions de recherche en découlent, qui sauront, on l'espère, intéresser autant les logiciens que les informaticiens!
[1] L. Santocanale, A calculus of circular proofs and its categorical semantics, in: M. Nielsen, U. Engberg (eds.), FOSSACS 2002, No. 2303 in LNCS, Springer, 2002.

 

Liste des séminaires de l'année ...
[2002] [2003] [2004] [2005] [2006] [2007] [2008] [2009] [2010] [2011] [2012]

EL, le 5 décembre 2013