From Linear Logic to Cyclic Sharing

2019/04/15 by Masahito Hasegawa
Computer Science · #cs.LO #cs.PL

paper · pdf · doi:10.4204/eptcs.292.3

published as EPTCS 292, 2019, pp. 31-42 · In Proceedings Linearity-TLLA 2018, arXiv:1904.06159

arxiv created 2019/04/15 · arxiv updated 2019/04/16

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.

Citations

• Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications