Séminaire de rentrée, 20 septembre 2013
Exposés
 10:00: Michele Basaldella, 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 proofsystem for this language is given by a sequent calculus with infinitary rules of inferences. Firstorder 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 soundnessandcompleteness theorem for derivations in the infinitary logic with respect to this kind of semantics.
 14:00: Clément Aubert, Proof circuits and parallel cutelimination in logarithmic space

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