Polarized proof nets with cycles and fixpoints semantics

Abstract

Starting from Laurent's work on Polarized Linear Logic, we define a new polarized linear deduction system which handles recursion. This is achieved by extending the cut-rule, in such a way that iteration unrolling is achieved by cut-elimination. The proof nets counterpart of this extension is obtained by allowing oriented cycles, which had no meaning in usual polarized linear logic. We also free proof nets from additional constraints, leading up to a correctness criterion as straight-forward as possible (since almost all proof structures are correct). Our system has a sound semantics expressed in traced models. © Springer-Verlag Berlin Heidelberg 2003.