We present a simple cut-elimination procedure for MALL proof nets with monomial weights (à la Girard) a 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.
Maieli, R. (2008). Cut Elimination for Monomial Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic. Roma : I.A.C. - Istituto per le Applicazioni del Calcolo.
Cut Elimination for Monomial Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic
MAIELI, ROBERTO
2008-01-01
Abstract
We present a simple cut-elimination procedure for MALL proof nets with monomial weights (à la Girard) a 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.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
