@inbook{9ceac842dd084e0eb85fbdfa9db9fb81,
title = "On proof nets for multiplicative linear logic with units",
abstract = "In this paper we present a theory of proof nets for full multiplicative linear logic, including the two units. It naturally extends the well-known theory of unit-free multiplicative proof nets. A linking is no longer a set of axiom links but a tree in which the axiom links are subtrees. These trees will be identified according to an equivalence relation based on a simple form of graph rewriting. We show the standard results of sequentialization and strong normalization of cut elimination. Furthermore, the identifications enforced on proofs are such that the proof nets, as they are presented here, form the arrows of the free (symmetric) *-autonomous category.",
author = "Lutz Stra{\ss}burger and Fran{\c c}ois Lamarche",
year = "2004",
month = jan,
day = "1",
doi = "10.1007/978-3-540-30124-0\_14",
language = "English",
isbn = "3540230246",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "145--159",
editor = "Jerzy Marcinkowski and Andrzej Tarlecki",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
}