Eduardo Bonelli

Sharing and Linear Logic with Restricted Access

2025 · Lecture notes in computer science

Abstract The two Girard translations provide two different means of obtaining embeddings of Intuitionistic Logic into Linear Logic, corresponding to different lambda-calculus calling mechanisms. The translations, mapping $$A\rightarrow B$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>A</mml:mi> <mml:mo>→</mml:mo> <mml:mi>B</mml:mi> …