Free Deduction Process Calculus
In sequent-style proof systems, natural deduction combines introduction and elimination rules, while Gentzen’s LK is defined by dual introduction forms. The λ-calculus and λμ̃-calculus capture the computational essence of normalization in these frameworks. However, there are also logical systems like Parigot’s “Free Deduction” (FD) which rely exclusively on elimination rules. While the term assignment system and semantics of such a calculus can be understood in terms of its translation to either ND or LK, we lack a standalone semantics for such a framework.
In this thesis, we present a modern reconstruction of Free Deduction, titled πFD, as a process calculus grounded in linear logic - akin to Negri’s “Uniform Calculus for Classical Linear Logic” (UCL). By embedding explicit μ and ṽ-style activations directly into the typing rules and equipping each statement with its own continuation process, πFD enables a unified treatment of synchronous and asynchronous communication. This yields an alternative design for session-typed disciplines that diverges from Girard’s linear logic.
We formalize the metatheory of πFD within Rocq, providing mechanized proofs for type safety and the Church-Rosser property. These results establish a rigorous foundation for reasoning about concurrent communication in elimination-based systems. Ultimately, πFD deepens the Curry-Howard correspondence for parallel and communication-based calculi, offering new insights into the relationship between logical elimination and session-based concurrency.