Cited by Lee Sonogan
Abstract by DELIA KESNER
This paper introduces a functional term calculus, called pn, that captures the essence of the operational semantics of Intuitionistic Linear Logic Proof-Nets with a faithful degree of granularity, both statically and dynamically. On the static side, we identify an equivalence relation on pn-terms which is sound and complete with respect to the classical notion of structural equivalence for proof-nets. On the dynamic side, we show that every single (exponential) step in the term calculus translates to a different single (exponential) step in the graphical formalism, thus capturing the original Girard’s granularity of proof-nets but on the level of terms. We also show some fundamental properties of the calculus such as confluence, strong normalization, preservation of β-strong normalization and the existence of a strong bisimulation that captures pairs of pn-terms having the same graph reduction.
Publication: Université de Paris
Pub Date: Doi: https://www.irif.fr/~kesner/papers/popl22.pdf
Keywords: lambda-calculus, explicit substitutions, linear logic, proof-nets
https://www.irif.fr/~kesner/papers/popl22.pdf (Plenty more sections and references in this research article)
https://www.patreon.com/GROOVYGORDS
https://entertainmentcultureonline.com/