Séminaire Logique et Interactions

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

À venir

Vendredi 20 septembre 2013 à 10h

Michele Basaldella (IML)
An interactive semantics for classical arithmethic

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.

Vendredi 20 septembre 2013 à 14h

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

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.

Jeudi 26 septembre 2013

Séminaire Chocola.

Vendredi 27 septembre 2013 à 14h

Matteo Acclavio (IML)

Jeudi 3 octobre 2013 à 14h

Michele Alberti (IML)

Archives

1994, 1995, 1996, 1997, 1998, 1999, 2000, 00-01, 01-02, 02-03, 03-04, 04-05, 05-06, 06-07, 07-08, 08-09, 09-10 10-11 11-12

LDP

Membres

Recherche

Collaborations

Master