On the denotation of circular and non-wellfounded proofs in linear logic with fixed points

This paper investigates the denotational invariants of non-wellfounded and circular proofs of linear logic with least and greatest fixed points, μLL, by providing a categorical semantics. More precisely the paper successively introduces semantics for (i) non-wellfounded pre-proofs, be they valid or not, (ii) valid pre-proofs exploiting their validity condition by considering an orthogonality construction on the given categorical model and finally (iii) circular strongly valid pre-proofs, exploiting both validity and regularity in order to define inductively the interpretation. Then the paper investigates the semantical content of the translation from finitary proofs to non-wellfounded proofs and, conversely, from (strongly valid) circular proofs to finitary proofs, showing that both translations preserve the interpretation.