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 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.

14:00: Clément Aubert, 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.