### ClĂ©ment Aubert (LIPN - Univ. Paris 13), Proof circuits and others parallel models of computation.

#### Schedule

- Feb. 2, 2012, 16:00 - 16:30

#### Abstract

Proof circuits [Aubert, 11] are a clear and intuitive presentation of the Boolean
proof nets [Terui, 04] in a uniform framework [Mogbil-Rahli, 07] : we define *pieces*
as a set of links and edges of a unbounded variant of *Multiplicative Linear Logic*
representing Boolean constants, n-ary disjunctions and conjonctions, negation and
mechanisms such as deletion and duplication. Thoses pieces may be "plugged"
together to obtain *proof circuits* : *MLLu* uniform Boolean proof nets whose
size and depth are implicitly bounded and whose parralel normalization matches
up evaluation in Boolean circuits. This light presentation allows sublogarithmic
translation and simulation between Boolean circuits and proof circuits, lightens
the size of the latter and preserves all the good properties concerning complexity.
We conclude by giving the rst hints toward a full correspondence between proof
circuits and alternating Turing machines, enlarging the correspondence between
parallel models of computation.