Cut Elimination for Monomial Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic
Roberto Maieli · 2007
We present a simple cut-elimination procedure for MALL proof nets with monomial weights (` a la Girard) and explicit contraction links, based on an almost local cut reduction steps. This procedure preserves correctness of proof nets and it is strong normalizing and confluent.