A fine-grained computational interpretation of Girard's intuitionistic proof-nets

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.