Open Publishing Association, Electronic Proceedings in Theoretical Computer Science, (75), p. 15-27, 2012
DOI: 10.4204/eptcs.75.2
Full text: Download
Cut-elimination in proof nets for Multiplicative Linear Logic and evaluation in Boolean circuits may be linked using the proofs-as-programs correspondence. Those two models of parallel computation offer a framework where we can study uniformity and implicit complexity. Boolean proof nets were introduced by [Terui, 2004] and studied by [Mogbil & Rahli, 2007] to compare the computational power of proof nets and of Boolean circuits. They established inclusions between classes of complexity that could not be extended to sublogarithmic classes as AC0 and NC1. By restricting the way Boolean proof nets are built we prove anew those inclusion results -- in an uniform framework -- and extend them to small classes of complexity.