pith. sign in

arxiv: 1907.03631 · v1 · pith:LLY4YGHEnew · submitted 2019-07-08 · 💻 cs.LO

unicode{8523} means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs

Federico Aschieri , Francesco A. Genco This is my paper

Pith reviewed 2026-05-25 00:46 UTC · model grok-4.3

classification 💻 cs.LO
keywords multiplicative linear logicconcurrent functional programminglambda calculusnatural deductionsubject reductionstrong normalizationconfluenceproofs as processes
0
0 comments X

The pith

Multiplicative linear logic is isomorphic to the typing system of λ_𝜋, a concurrent extension of the lambda calculus.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that a linear multiple-conclusion natural deduction system for multiplicative linear logic is isomorphic to the typing rules of λ_𝜋, an extension of the lambda calculus with parallelism and communication primitives. This isomorphism transfers logical properties to the programming language. A sympathetic reader would care because it yields a typed concurrent functional language with subject reduction, progress, strong normalization, and confluence. The work follows the proofs-as-processes idea to link logic directly to safe concurrent computation.

Core claim

We present an interpretation of multiplicative linear logic as a typing system for concurrent functional programming. In particular, we study a linear multiple-conclusion natural deduction system and show it is isomorphic to a simple and natural extension of λ-calculus with parallelism and communication primitives, called λ_𝜋. We prove that λ_𝜋 satisfies subject reduction, progress, strong normalization and confluence.

What carries the argument

The isomorphism between the linear multiple-conclusion natural deduction system for multiplicative linear logic and the typing rules of λ_𝜋, which transfers logical properties to concurrent programs.

If this is right

  • λ_𝜋 satisfies subject reduction, so types are preserved under reduction.
  • Progress holds, so well-typed λ_𝜋 terms never get stuck.
  • Strong normalization and confluence hold for λ_𝜋.
  • Concurrent functional programs typed by the logic inherit logical consistency guarantees.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same isomorphism technique could be applied to other linear logic fragments to obtain typed languages for different concurrency models.
  • Proof search in the natural deduction system might serve as a method to synthesize concurrent programs.
  • The correspondence suggests that adding new communication primitives could be checked by extending the natural deduction rules while preserving normalization.

Load-bearing premise

The linear multiple-conclusion natural deduction system for multiplicative linear logic is isomorphic to the typing rules of the λ_𝜋 calculus.

What would settle it

A reduction sequence starting from a well-typed λ_𝜋 term that reaches an ill-typed term would falsify subject reduction.

read the original abstract

Along the lines of the Abramsky ``Proofs-as-Processes'' program, we present an interpretation of multiplicative linear logic as typing system for concurrent functional programming. In particular, we study a linear multiple-conclusion natural deduction system and show it is isomorphic to a simple and natural extension of $\lambda$-calculus with parallelism and communication primitives, called $\lambda_{\unicode{8523}}$. We shall prove that $\lambda_{\unicode{8523}}$ satisfies all the desirable properties for a typed programming language: subject reduction, progress, strong normalization and confluence.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper claims that a linear multiple-conclusion natural deduction system for multiplicative linear logic is isomorphic to the typing rules of λ_𝜋 (an extension of the λ-calculus with parallelism and communication primitives denoted by 𝜋), and that this correspondence allows transfer of logical properties to prove that λ_𝜋 satisfies subject reduction, progress, strong normalization, and confluence.

Significance. If the isomorphism and meta-theoretic proofs hold, the work extends the proofs-as-processes paradigm with a natural-deduction presentation of MLL that directly types concurrent functional programs, supplying a typed language with strong normalization and confluence guarantees.

major comments (1)
  1. [Abstract] Abstract, paragraph 2: the asserted isomorphism between the linear multiple-conclusion natural deduction system for MLL and the typing rules of λ_𝜋 is load-bearing for all four claimed properties. No explicit bijection is supplied for the rules (including multiple conclusions and the new parallel operator), so it is impossible to verify that subject reduction and strong normalization transfer without gaps in the correspondence.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for highlighting this point about the explicitness of the claimed isomorphism. We address the comment below and will revise the paper to strengthen the presentation.

read point-by-point responses

  1. Referee: [Abstract] Abstract, paragraph 2: the asserted isomorphism between the linear multiple-conclusion natural deduction system for MLL and the typing rules of λ_𝜋 is load-bearing for all four claimed properties. No explicit bijection is supplied for the rules (including multiple conclusions and the new parallel operator), so it is impossible to verify that subject reduction and strong normalization transfer without gaps in the correspondence.

    Authors: We agree that the manuscript would benefit from an explicit statement of the bijection. The natural deduction rules for the linear multiple-conclusion system are presented in direct parallel with the typing rules of λ_𝜋 (with the parallel operator 𝜋 corresponding to the multiplicative rules that introduce multiple conclusions), but we acknowledge that a dedicated mapping or table would make the one-to-one correspondence, including handling of multiple conclusions, fully transparent. We will add a new subsection (or table) in the revised version that enumerates the bijection rule-by-rule and explains how the meta-theoretic properties transfer via this correspondence. revision: yes

Circularity Check

0 steps flagged

No circularity: isomorphism and meta-theoretic properties established independently

full rationale

The paper defines a linear multiple-conclusion natural deduction system for MLL and claims to exhibit an isomorphism to the typing rules of the extended λ_𝜋 calculus, after which subject reduction, progress, strong normalization and confluence are proved for the programming language. No equations, definitions or derivations in the abstract or described structure reduce any claimed result to a fitted parameter, a self-citation chain, or an input by construction. The central correspondence is presented as a theorem to be proved rather than presupposed, and the subsequent meta-theoretic results are independent derivations that do not collapse into the inputs. This is a standard, self-contained proof-theoretic development in the proofs-as-processes tradition.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Only the abstract is available; the paper relies on standard properties of linear logic and natural deduction that are not detailed here. No free parameters, invented entities, or ad-hoc axioms are visible in the provided text.

pith-pipeline@v0.9.0 · 5619 in / 1064 out tokens · 18499 ms · 2026-05-25T00:46:53.357184+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

33 extracted references · 33 canonical work pages

  1. [1]

    Proofs as processes

    Samson Abramsky. Proofs as processes. Theor. Comput. Sci. , 135(1):5–9, 1994

    work page 1994

  2. [2]

    Gay, and Rajagopal Nagarajan

    Samson Abramsky, Simon J. Gay, and Rajagopal Nagarajan. Interaction categories and the foundations of typed concurrent programming. In Proceedings of the NATO Advanced Study Institute on Deductive Program Design, Marktoberdorf , Germany , pages 35–113, 1996

    work page 1996

  3. [3]

    Federico Aschieri, Agata Ciabattoni, and Francesco A. G enco. G¨ odel logic: from natural deduction to parallel computation. In LICS 2017 , pages 1–12, 2017

    work page 2017

  4. [4]

    Federico Aschieri, Agata Ciabattoni, and Francesco A. G enco. Classical proofs as parallel programs. In GandALF 2018 , pages 43–57, 2018

    work page 2018

  5. [5]

    On natural dedu ction in classical first-order logic: Curry–howard correspondence, strong normalization and he rbrand’s theorem

    Federico Aschieri and Margherita Zorzi. On natural dedu ction in classical first-order logic: Curry–howard correspondence, strong normalization and he rbrand’s theorem. Theoretical Computer Science , 625:125–146, 2016. 35

    work page 2016

  6. [6]

    Hypersequents, logical consequence and in termediate logics for concur- rency

    Arnon Avron. Hypersequents, logical consequence and in termediate logics for concur- rency. Annals of Mathematics and Artificial Intelligence , 4(3):225–248, 1991

    work page 1991

  7. [7]

    Gianluigi Bellin and Philip J. Scott. On the pi-calculus and linear logic. Theor. Comput. Sci., 135(1):11–65, 1994

    work page 1994

  8. [8]

    Asynchrony and the Pi-calculus

    G´ erard Boudol. Asynchrony and the Pi-calculus. Resear ch Report RR-1702, INRIA, 1992

    work page 1992

  9. [9]

    Session types as intuit ionistic linear propositions

    Lu ´ ıs Caires and Frank Pfenning. Session types as intuit ionistic linear propositions. In CONCUR 2010 , pages 222–236, 2010

    work page 2010

  10. [10]

    Multiparty session types as coherence proofs

    Marco Carbone, Fabrizio Montesi, Carsten Sch¨ urmann, and Nobuko Yoshida. Multiparty session types as coherence proofs. Acta Inf. , 54(3):243–269, 2017

    work page 2017

  11. [11]

    Existential instantiation and normal ization in sequent natural deduction

    Carlo Cellucci. Existential instantiation and normal ization in sequent natural deduction. Annals of Pure and Applied Logic , 58(2):111 – 148, 1992

    work page 1992

  12. [12]

    Ornela Dardha and Simon J. Gay. A new linear logic for dea dlock-free session-typed processes. In Foundations of Software Science and Computation Structures - 21st Inter- national Conference, FOSSACS 2018, Held as Part of the Europea n Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, p...

    work page 2018

  13. [13]

    Gay and Vasco Thudichum Vasconcelos

    Simon J. Gay and Vasco Thudichum Vasconcelos. Linear ty pe theory for asynchronous session types. J. Funct. Program., 20(1):19–50, 2010

    work page 2010

  14. [14]

    Linear logic

    Jean-Yves Girard. Linear logic. Theoretical computer science, 50(1):1–101, 1987

    work page 1987

  15. [15]

    Proofs and Types

    Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Cambridge University Press, 1989

    work page 1989

  16. [16]

    An exact corresponden ce between a typed pi-calculus and polarised proof-nets

    Kohei Honda and Olivier Laurent. An exact corresponden ce between a typed pi-calculus and polarised proof-nets. Theor. Comput. Sci. , 411(22-24):2223–2238, 2010

    work page 2010

  17. [17]

    Multiple conclus ion linear logic: Cut elimination and more

    Harley Eades III and Valeria de Paiva. Multiple conclus ion linear logic: Cut elimination and more. In Logical Foundations of Computer Science - International Symp osium, LFCS 2016, Deerfield Beach, FL, USA, January 4-7, 2016. Proceeding s, pages 90–105, 2016

    work page 2016

  18. [18]

    Bet ter late than never: a fully- abstract semantics for classical processes

    Wen Kokke, Fabrizio Montesi, and Marco Peressotti. Bet ter late than never: a fully- abstract semantics for classical processes. In POPL 2019 , pages 24:1–24:29, 2019

    work page 2019

  19. [19]

    Classical realizability

    Jean-Louis Krivine. Classical realizability. Interactive models of computation and program behavior, Panoramas et synth` eses , pages 197–229, 2009

    work page 2009

  20. [20]

    Lolliproc: to concur rency from classical linear logic via curry-howard and control

    Karl Mazurak and Steve Zdancewic. Lolliproc: to concur rency from classical linear logic via curry-howard and control. In Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, Septem- ber 27-29, 2010 , pages 39–50, 2010

    work page 2010

  21. [21]

    On asynchrony in na me-passing calculi

    Massimo Merro and Davide Sangiorgi. On asynchrony in na me-passing calculi. Mathe- matical Structures in Computer Science , 14(5):715–767, 2004. 36

    work page 2004

  22. [22]

    A Calculus of Communicating Systems , volume 92 of Lecture Notes in Computer Science

    Robin Milner. A Calculus of Communicating Systems , volume 92 of Lecture Notes in Computer Science . Springer, 1980

    work page 1980

  23. [23]

    Lectures on a calculus for communicating systems

    Robin Milner. Lectures on a calculus for communicating systems. In Seminar on Con- currency, pages 197–219. Springer, 1984

    work page 1984

  24. [24]

    A calcu lus of mobile processes, I

    Robin Milner, Joachim Parrow, and David Walker. A calcu lus of mobile processes, I. Inf. Comput. , 100(1):1–40, 1992

    work page 1992

  25. [25]

    Free deduction: An analysis of ”comput ations” in classical logic

    Michel Parigot. Free deduction: An analysis of ”comput ations” in classical logic. In Logic Programming, pages 361–380, 1991

    work page 1991

  26. [26]

    Lambda-mu-calculus: An algorithmic i nterpretation of classical natural deduction

    Michel Parigot. Lambda-mu-calculus: An algorithmic i nterpretation of classical natural deduction. In LPAR 1992, pages 190–201, 1992

    work page 1992

  27. [27]

    P´ erez, Lu ´ ıs Caires, Frank Pfenning, and Bern ardo Toninho

    Jorge A. P´ erez, Lu ´ ıs Caires, Frank Pfenning, and Bern ardo Toninho. Linear logical relations for session-based concurrency. In Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part o f the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Ta llinn, Estonia, March 24 - April 1, 201...

    work page 2012

  28. [28]

    Ideas and results in proof theory

    Dag Prawitz. Ideas and results in proof theory. In Proceedings of the Second Scandinavian Logic Symposium, 1971

    work page 1971

  29. [29]

    A message-passing i nterpretation of adjoint logic

    Klaas Pruiksma and Frank Pfenning. A message-passing i nterpretation of adjoint logic. In Proceedings Programming Language Approaches to Concurrency- and Communication- cEntric Software, PLACES@ETAPS 2019, Prague, Czech Republic, 7th April 2019. , pages 60–79, 2019

    work page 2019

  30. [30]

    Expressing mobility in process algebras: first-order and hi gher-order paradigms

    Davide Sangiorgi. Expressing mobility in process algebras: first-order and hi gher-order paradigms. PhD thesis, The University of Edinburgh, 1993

    work page 1993

  31. [31]

    Hi gher-order processes, functions, and sessions: A monadic integration

    Bernardo Toninho, Lu ´ ıs Caires, and Frank Pfenning. Hi gher-order processes, functions, and sessions: A monadic integration. In ESOP 2013 , pages 350–369, 2013

    work page 2013

  32. [32]

    Propositions as sessions

    Philip Wadler. Propositions as sessions. ICFP 2012 , 24:384–418, 2012

    work page 2012

  33. [33]

    Propositions as types

    Philip Wadler. Propositions as types. Communications of the ACM , 58(12):75–84, 2015. 37

    work page 2015