From Linear Logic to Cyclic Sharing

Masahito Hasegawa
(RIMS, Kyoto University)

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.

In Thomas Ehrhard, Maribel Fernández, Valeria de Paiva and Lorenzo Tortora de Falco: Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications (Linearity-TLLA 2018), Oxford, UK, 7-8 July 2018, Electronic Proceedings in Theoretical Computer Science 292, pp. 31–42.
Published: 15th April 2019.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: