# From Linear Logic to Cyclic Sharing

## TL;DR

This paper introduces a novel translation from Multiplicative Exponential Linear Logic to a simply-typed lambda calculus with cyclic sharing, combining ideas from category theory and the Geometry of Interaction.

## Contribution

It provides a new categorical insight and a practical translation method connecting linear logic with cyclic sharing in lambda calculus.

## Key findings

- The translation is derived from the Int-construction on traced monoidal categories.
- It combines call-by-name CPS translation with Geometry of Interaction.
- The approach offers a new perspective on the relationship between linear logic and lambda calculus.

## Abstract

We present a translation from Multiplicative Exponential Linear Logic to a simply-typed lambda calculus with cyclic sharing. This translation is derived from a simple observation on the Int-construction on traced monoidal categories. It turns out that the translation is a mixture of the call-by-name CPS translation and the Geometry of Interaction-based interpretation.