pith. sign in

arxiv: 2403.18508 · v4 · submitted 2024-03-27 · 💻 cs.LO

On Propositional Dynamic Logic and Concurrency

Matteo Acclavio , Fabrizio Montesi , Marco Peressotti This is my paper

Pith reviewed 2026-05-24 03:38 UTC · model grok-4.3

classification 💻 cs.LO
keywords propositional dynamic logicoperational semanticsconcurrencysequent calculuscut-eliminationCCSchoreographic programminginterleaving
0
0 comments X

The pith

Operational propositional dynamic logic models concurrent programs by distinguishing them from traces generated by any operational semantics.

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

Traditional propositional dynamic logic struggles with concurrency because it represents programs as sets of traces inside Kleene algebras, where equality becomes undecidable once commutations for interleaving are required. This paper introduces operational propositional dynamic logic that keeps programs separate from the traces they produce. Traces are generated on demand by an arbitrary operational semantics supplied as a parameter. The authors first prove cut-elimination for a finitely-branching non-wellfounded sequent calculus for ordinary PDL and then transfer the same results to the new framework. They illustrate the method on CCS, where parallel composition produces interleaving, and on choreographic programming, where out-of-order execution produces interleaving.

Core claim

The central claim is that propositional dynamic logic can be generalised to operational propositional dynamic logic by separating programs from their traces, with traces produced by an arbitrary operational semantics taken as a parameter; this separation permits a sequent calculus with cut-elimination to be proved once for PDL and then reused for OPDL without further restrictions on the semantics.

What carries the argument

The separation of programs from traces, where traces are generated by an arbitrary operational semantics supplied as a parameter to the logic.

If this is right

  • Cut-elimination holds for the sequent calculus of PDL and extends directly to OPDL.
  • Adequacy results proved for PDL carry over to any instance of OPDL.
  • Interleaving arising from parallel composition in CCS can be expressed inside OPDL.
  • Interleaving arising from out-of-order execution in choreographic programming can be expressed inside OPDL.

Where Pith is reading between the lines

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

  • The same parameterised construction could be instantiated for other process calculi such as the pi-calculus by supplying the corresponding reduction rules.
  • The separation of syntax from traces may allow OPDL to be combined with data logics without forcing trace equality decisions.
  • Proof assistants could be used to certify cut-elimination once the operational rules are encoded as a parameter.

Load-bearing premise

An arbitrary operational semantics can be supplied as a parameter while still allowing the sequent calculus and cut-elimination results to transfer directly to OPDL without additional restrictions on the semantics.

What would settle it

An operational semantics for which the sequent calculus fails to admit cut-elimination or fails to be adequate for the intended program semantics.

Figures

Figures reproduced from arXiv: 2403.18508 by Fabrizio Montesi, Marco Peressotti, Matteo Acclavio.

Figure 1
Figure 1. Figure 1: Grammar generating formulas After recalling the axiomatization and semantics of PDL in Section 2, in Section 3 we provide a proof of its soundness and completeness with respect to the sequent calculus introduced in [20]. For this purpose, we provide the first cut￾elimination result for this non-wellfounded calculus, by adapting the technique developed in [2].4 This allows us to prove our results by reasoni… view at source ↗
Figure 2
Figure 2. Figure 2: Axioms and rules for Propositional Dynamic Logic. [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Inductive definition of the meaning of compound form [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Sequent calculus rules of the sequent system LPD [PITH_FULL_IMAGE:figures/full_fig_p006_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Non-trivial derivations of the axioms of PDL in LPD. [PITH_FULL_IMAGE:figures/full_fig_p009_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Derivability of the loop invariance rule in LPD [PITH_FULL_IMAGE:figures/full_fig_p009_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Cut-elimination steps in LPD (with k restricted on ∈ I). The steps in the bo om-most row are called commutative. 3.3 Cut-Elimination in LPDcut In order to prove cut-elimination in LPD, we adapt the proof in [2, 3] to define an infinitary rewriting defined from the cut-elimination steps in [PITH_FULL_IMAGE:figures/full_fig_p010_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Derivations proving that if ⊢pLPD Γ, [ ∗ ] , then ⊢pLPD Γ, [ ] for any ∈ N. Remark 20 (Fisher-Ladner Analyticity). By rules inspection, each sequent occurring in a derivation D ∈ LPD with conclusion Γ is a subset of FL(Γ) = Ð ∈Γ FL(). More precisely, if Δ is a premise of a rule with conclusion Γ, then FL(Δ) ⊆ FL(Γ). Theorem 21. Let Γ be a sequent. Then ⊢pLPD Γ iff ⊢PDL Γ. Proof. Completeness of pLPD with r… view at source ↗
Figure 9
Figure 9. Figure 9: Derivation in pLOPD of the axiom OAtom, where we are assuming {1, . . . , } = { ∈ L | }. The case = 0 is trivial and it is omi ed. ⊢ Γ, Δ ′ , Σ ′ r2 ⊢ Γ, Δ ′ , Σ r1 ⊢ Γ, Δ, Σ ≡ ⊢ Γ, Δ ′ , Σ ′ r1 ⊢ Γ, Δ, Σ ′ r2 ⊢ Γ, Δ, Σ Γ ′ , r2 Γ, Δ, r1 Γ, Δ, Σ ≡ Γ ′ , Δ, r1 Γ ′ , Δ, Σ r2 Γ, Δ, Σ Γ1, Γ2, r2 Γ1, Γ2, Δ Γ3, r1 Γ1, Γ2, Γ3, Δ, Σ ≡ Γ1, Γ2, Γ3, r1 Γ2, Γ3, Σ r2 Γ1, Γ2, Γ3, Δ, Σ [PITH_FULL_IMAGE:figures/full_fig_… view at source ↗
Figure 10
Figure 10. Figure 10: Independent rule permutations. such a rule in order to distinguish the branching due to interleaving concurrency from the branching due to internal choices of the system. More precisely, using the terminology from [6, 36, 54], interleaving concurrency is a form of ‘don’t care’ non-determinism, depending on inessential choices introduced by the syntax because of its limitations in handling concurrency, whi… view at source ↗
Figure 11
Figure 11. Figure 11: Additional cut-elimination step in LOPD. [PITH_FULL_IMAGE:figures/full_fig_p019_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Both syntax and semantics are standard and we brie [PITH_FULL_IMAGE:figures/full_fig_p019_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: The derivation proving 1 ∼Tr 2. par1 allows | to perform a transition where performs an action (evolving into ′ ) independently from and symmetrically for rule par2. Rule com describes transitions where and synchronise by performing matching actions. To model that synchronisations are binary, transitions derived with this rule are given the label which is separate from Act and is traditionally used in pro… view at source ↗
Figure 14
Figure 14. Figure 14: Syntax of choreographies. atomic cond-then if p. then1 else2 p.? 1 cond-else if p. then1 else2 p.? 2 call q: p1 : ; . . . ; p : ; if def = and pn() = {q, p1, . . . , p} i ; if delay-i ; ; ′ if ′ and pn() ∩ pn() = ∅ delay-cond if p. then1 else2; if p. then ′ 1 else ′ 2 ; if [PITH_FULL_IMAGE:figures/full_fig_p023_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: Operational semantics of symbolic choreographies [PITH_FULL_IMAGE:figures/full_fig_p023_15.png] view at source ↗
Figure 16
Figure 16. Figure 16: The derivation proving 1; 2; ∼Tr 2; 1; whenever pn( 2 ) ∩ ( {p} ∪ pn( 1 ) ) = ∅ (because of the out-of-order execution). successful. Likewise, p.? represents a negative test. Test instructions are not part of the language [64]; we decided to include them to illustrate the use of tests in OPDL. The term 0 denotes the inactive choreography and has no transitions. A term ; denotes the sequential com￾position… view at source ↗
Figure 17
Figure 17. Figure 17: The derivations proving if p. then( 2; 1;1 ) else( 2;2 ) ∼Tr 2; if p. then 1;1 else2 whenever pn( 2 ) ∩ ( {p} ∪ pn( 1 ) ) = ∅ (because of the out-of-order execution), where † = h O i + 2 × w. semantics of the programs under consideration. The result, OPDL, subsumes a number of previous extensions of PDL by seeing them as particular instantiations of this schema. Furthermore, OPDL can be instantiated for p… view at source ↗
read the original abstract

Dynamic logic is a powerful approach to reasoning about programs and their executions, obtained by extending classical logic with modalities that can express program executions as formulas. However, the use of dynamic logic in the setting of concurrency has proved problematic because of the challenge of capturing interleaving. This challenge stems from the fact that, traditionally, programs are represented by their sets of traces. These sets are then expressed as elements of a Kleene algebra, for which it is not possible to decide equality in the presence of the commutations required to model interleaving. In this work, we generalise propositional dynamic logic (PDL) to a logic framework we call operational propositional dynamic logic (OPDL), which departs from tradition by distinguishing programs from their traces. Traces are generated by an arbitrary operational semantics that we take as a parameter, making our approach applicable to different program syntaxes and semantics. To develop our framework, we provide the first proof of cut-elimination for a finitely-branching non-wellfounded sequent calculus for PDL. Thanks to this result we can effortlessly prove adequacy for PDL, and extend these results to OPDL. We conclude by discussing OPDL for two representative cases of concurrency: the Calculus of Communicating Systems (CCS), where interleaving is obtained by parallel composition, and Choreographic Programming, where interleaving is obtained by out-of-order execution.

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

2 major / 1 minor

Summary. The paper introduces operational propositional dynamic logic (OPDL) by generalizing PDL to distinguish programs from traces, where traces are generated by an arbitrary operational semantics taken as a parameter. It supplies the first cut-elimination proof for a finitely-branching non-wellfounded sequent calculus for standard PDL, derives adequacy from it, and extends both results to OPDL. The framework is then applied to concurrency examples: CCS (interleaving via parallel composition) and choreographic programming (interleaving via out-of-order execution).

Significance. If the cut-elimination and adequacy results transfer to OPDL without additional restrictions on the operational semantics parameter, the work would provide a flexible, semantics-parameterized approach to dynamic logic that sidesteps undecidability problems with Kleene algebras under commutation. The cut-elimination proof for the non-wellfounded PDL calculus itself constitutes a technical contribution.

major comments (2)
  1. [OPDL definition and extension of cut-elimination] The central claim that the PDL cut-elimination result 'effortlessly' extends to OPDL for an arbitrary operational semantics (abstract and OPDL definition section) is load-bearing but unsupported without side conditions: the PDL calculus is explicitly finitely-branching, yet nothing in the parameterization enforces that the supplied operational semantics preserves finite branching or avoids infinite nondeterminism that would break the non-wellfounded cut-elimination argument.
  2. [Sequent calculus for OPDL] § on the sequent calculus for OPDL: the interaction between the modal operators and the trace-generation rules from the arbitrary semantics is not shown to preserve the invariants (finite branching, non-wellfoundedness handling) used in the PDL cut-elimination proof; a concrete counter-example semantics violating these would falsify the transfer.
minor comments (1)
  1. [Abstract] The abstract states 'first proof of cut-elimination' for the PDL calculus without citing or briefly contrasting prior non-wellfounded calculi for PDL or related modal logics.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for identifying points where additional clarification is needed regarding the assumptions on operational semantics. We address the major comments below.

read point-by-point responses

  1. Referee: The central claim that the PDL cut-elimination result 'effortlessly' extends to OPDL for an arbitrary operational semantics (abstract and OPDL definition section) is load-bearing but unsupported without side conditions: the PDL calculus is explicitly finitely-branching, yet nothing in the parameterization enforces that the supplied operational semantics preserves finite branching or avoids infinite nondeterminism that would break the non-wellfounded cut-elimination argument.

    Authors: We agree that the manuscript presents the operational semantics as a parameter without explicitly restricting it to finitely branching cases, even though the cut-elimination proof depends on this property. The framework is intended to apply to operational semantics that yield finitely branching transition relations, as is standard for the PDL calculus. In the revision we will add an explicit side condition to the definition of OPDL requiring finite branching and update the abstract and OPDL definition section to state that the cut-elimination and adequacy results hold under this assumption. revision: yes

  2. Referee: § on the sequent calculus for OPDL: the interaction between the modal operators and the trace-generation rules from the arbitrary semantics is not shown to preserve the invariants (finite branching, non-wellfoundedness handling) used in the PDL cut-elimination proof; a concrete counter-example semantics violating these would falsify the transfer.

    Authors: The sequent calculus for OPDL extends the PDL rules by interpreting the modal operators directly via the trace-generation rules of the supplied operational semantics. Because the cut-elimination argument is structural and depends only on finite branching of the transition relation (an invariant preserved by any finitely branching operational semantics), the same proof carries over without change. We will insert a short explanatory paragraph in the sequent calculus for OPDL section making this preservation explicit and noting that the finite-branching side condition suffices to maintain the required invariants. revision: yes

Circularity Check

0 steps flagged

No circularity: new cut-elimination proof for PDL extended parametrically to OPDL

full rationale

The paper supplies an original cut-elimination argument for the finitely-branching non-wellfounded sequent calculus of PDL and then states that the same argument transfers to OPDL once an arbitrary operational semantics is supplied as a parameter. No equation or definition is shown to be equivalent to its own input by construction, no fitted quantity is relabeled as a prediction, and no load-bearing step reduces to a self-citation whose content is itself unverified. The derivation therefore remains self-contained; any question about whether the transfer truly holds for completely unrestricted semantics is a matter of proof correctness rather than circularity.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract supplies no explicit free parameters, axioms, or invented entities.

pith-pipeline@v0.9.0 · 5776 in / 1047 out tokens · 42927 ms · 2026-05-24T03:38:05.332182+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

83 extracted references · 83 canonical work pages

  1. [1]

    Matteo Acclavio and Davide Catta. 2023. Lorenzen-Style Strategies as Proof-Search Strategies. In Multi-Agent Systems, Vadim Malvone and Aniello Murano (Eds.). Springer Nature Switzerland, Cham, 150–166

    work page 2023

  2. [2]

    Matteo Acclavio, Gianluca Curzi, and Giulio Guerrieri. 2023. Infinitary cut-elimination via finite approximations . CoRR abs/2308.07789 (2023). https://doi.org/10.48550/ARXIV.2308.07789 arXiv:2308.07789

    work page doi:10.48550/arxiv.2308.07789 2023

  3. [3]

    Matteo Acclavio, Gianluca Curzi, and Giulio Guerrieri. 2024. Infinitary cut-elimination via finite approximations (extended version). arXiv:2308.07789 [cs.LO] https://arxiv.org/abs/2308.0 7789

    work page arXiv 2024

  4. [4]

    Fokkink, and Chris Verhoef

    Luca Aceto, Wan J. Fokkink, and Chris Verhoef. 2001. Stru ctural Operational Semantics. In Handbook of Process Algebra , Jan A. Bergstra, Alban Ponse, and Scott A. Smolka (Eds.). North-Holland / Elsevier , 197–292. https://doi.org/10.1016/B978-044482830-9/5 0021-7

    work page doi:10.1016/b978-044482830-9/5 2001

  5. [5]

    Luca Aceto, Anna Ingolfsdottir, and Jirí Srba. 2011. The algorithmics of bisimilarity . Cambridge University Press, 100–172

    work page 2011

  6. [6]

    Jean-Marc Andreoli. 1992. Logic programming with focus ing proofs in linear logic. Journal of logic and computation 2, 3 (1992), 297–347

    work page 1992

  7. [7]

    Arthur Azevedo de Amorim, Cheng Zhang, and Marco Gaboard i. 2025. Kleene Algebra with Commutativity Conditions Is Un decid- able. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025) (Leibniz International Proceedings in Informatics (L IPIcs), Vol. 326) , Jörg Endrullis and Sylvain Schmitz (Eds.). Schloss Dagstu hl – Leibniz-Zentrum für In...

    work page doi:10.4230/lipics.csl.2025.36 2025

  8. [8]

    David Baelde, Amina Doumane, and Alexis Saurin. 2016. In finitary Proof Theory: the Multiplicative Additive Case. In25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France (LIPIcs, Vol. 62) , Jean-Marc Talbot and Laurent Regnier (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 42:1–4 2:17...

    work page doi:10.4230/lipics.csl.2016.42 2016

  9. [9]

    Mario Benevides. 2017. Bisimilar and logically equival ent programs in PDL with parallel operator. Theoretical Computer Science 685 (2017), 23–45. https://doi.org/10.1016/j.tcs.2017.02.037 Logical and Semantic Frameworks with Applications. Manuscript submitted to ACM On Propositional Dynamic Logic and Concurrency 27

    work page doi:10.1016/j.tcs.2017.02.037 2017

  10. [10]

    Benevides and L

    Mario R.F. Benevides and L. Menasché Schechter. 2010. A Propositional Dynamic Logic for Concurrent Programs Basedon the /u1D70B-Calculus. Electronic Notes in Theoretical Computer Science 262 (2010), 49–64. https://doi.org/10.1016/j.entcs.201 0.04.005 Proceedings of the 6th Workshop on Methods for Modalities (M4M-6 2009)

    work page doi:10.1016/j.entcs.201 2010

  11. [11]

    Paul Brunet, Damien Pous, and Georg Struth. 2017. On Dec idability of Concurrent Kleene Algebra. In 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany ( LIPIcs, Vol. 85), Roland Meyer and Uwe Nestmann (Eds.). Schloss Dagstuhl - Le ibniz- Zentrum für Informatik, 28:1–28:15. https://doi.org/10. 4230/LIPICS...

    work page 2017

  12. [12]

    Nadia Busi, Maurizio Gabbrielli, and Gianluigi Zavatt aro. 2004. Comparing Recursion, Replication, and Iteratio n in Process Calculi. In Automata, Languages and Programming , Josep Díaz, Juhani Karhumäki, Arto Lepistö, and Donald San nella (Eds.). Springer Berlin Heidelberg, Berlin, Heidel- berg, 307–319

    work page 2004

  13. [13]

    Luís Caires and Frank Pfenning. 2010. Session Types as I ntuitionistic Linear Propositions. In CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-Septembe r 3, 2010. Proceedings (Lecture Notes in Computer Science, Vo l. 6269), Paul Gastin and François Laroussinie (Eds.). Springer, 222–236. https:// doi.o...

    work page doi:10.1007/978-3-642-15375-4_16 2010

  14. [14]

    Sjoerd Cranen, Jan Friso Groote, Jeroen J. A. Keiren, Fr ank P. M. Stappers, Erik P. de Vink, Wieger Wesselink, and Tim A. C. Willemse. 2013. An Overview of the mCRL2 Toolset and Its Recent Advances. In Tools and Algorithms for the Construction and Analysis of Sy stems - 19th International Conference, TACAS 2013, Held as Part of the Eur opean Joint Confer...

    work page doi:10.1007/978-3-642-36742-7_15 2013

  15. [15]

    Luís Cruz-Filipe, Eva Graversen, Lovro Lugovic, Fabri zio Montesi, and Marco Peressotti. 2023. Modular Compilati on for Higher-Order Functional Choreographies. In 37th European Conference on Object-Oriented Programming, E COOP 2023, July 17-21, 2023, Seattle, Washing- ton, United States (LIPIcs, Vol. 263) , Karim Ali and Guido Salvaneschi (Eds.). Schloss ...

    work page doi:10.4230/lipics.ecoop.2023.7 2023

  16. [16]

    Luís Cruz-Filipe, Eva Graversen, Fabrizio Montesi, an d Marco Peressotti. 2023. Reasoning About Choreographic Pr ograms. In Coordina- tion Models and Languages (Lecture Notes in Computer Scienc e, Vol. 13908) , Sung-Shik Jongmans and Antónia Lopes (Eds.). Springer, 14 4–162. https://doi.org/10.1007/978-3-031-35361-1_8

    work page doi:10.1007/978-3-031-35361-1_8 2023

  17. [17]

    Luís Cruz-Filipe and Fabrizio Montesi. 2017. Procedur al Choreographic Programming. In Formal Techniques for Distributed Objects, Components, and Systems - 37th IFIP WG 6.1 International Conference, FOR TE 2017, Held as Part of the 12th International Federated Conf erence on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerl and, June 19...

    work page doi:10.1007/978-3-319-60225-7_7 2017

  18. [18]

    Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peresso tti. 2023. A Formal Theory of Choreographic Programming. Journal of Automated Reasoning 67, 21 (2023), 1–34. https://doi.org/10.1007/s10817-023 -09665-3

    work page doi:10.1007/s10817-023 2023

  19. [19]

    Anupam Das and Marianna Girlando. 2022. Cyclic Proofs, Hypersequents, and Transitive Closure Logic. arXiv:2205. 08616 [cs.LO]

    work page 2022

  20. [20]

    Anupam Das and Marianna Girlando. 2022. Cyclic Proofs, Hypersequents, and Transitive Closure Logic. InAutomated Reasoning, Jasmin Blanchette, Laura Kovács, and Dirk Pattinson (Eds.). Springer Internat ional Publishing, Cham, 509–528

    work page 2022

  21. [21]

    Anupam Das and Marianna Girlando. 2023. Cyclic Hyperse quent System for Transitive Closure Logic. Journal of Automated Reasoning 67, 3 (2023),

    work page 2023

  22. [22]

    https://doi.org/10.1007/s10817-023-09675-1

    work page doi:10.1007/s10817-023-09675-1

  23. [23]

    Anupam Das and Sonia Marin. 2023. On Intuitionistic Dia monds (and Lack Thereof). In Automated Reasoning with Analytic Tableaux and Related Methods, Revantha Ramanayake and Josef Urban (Eds.). Springer Natu re Switzerland, Cham, 283–301

    work page 2023

  24. [24]

    Simon Docherty and Reuben N. S. Rowe. 2019. A Non-wellfo unded, Labelled Proof System for Propositional Dynamic Logic. In Automated Reasoning with Analytic Tableaux and Related Methods , Serenella Cerrito and Andrei Popescu (Eds.). Springer Int ernational Publishing, Cham, 335–352

    work page 2019

  25. [25]

    Thorsten Ehm, Bernhard Möller, and Georg Struth. 2004. Kleene Modules. In Relational and Kleene-Algebraic Methods in Computer Scien ce, Rudolf Berghammer, Bernhard Möller, and Georg Struth (Eds.). Spri nger Berlin Heidelberg, Berlin, Heidelberg, 112–123

    work page 2004

  26. [26]

    Ihor Filimonov, Ross Horne, Sjouke Mauw, and Zach Smith . 2019. Breaking Unlinkability of the ICAO 9303 Standard for e-Passports Using Bisim- ilarity. In Computer Security – ESORICS 2019 , Kazue Sako, Steve Schneider, and Peter Y. A. Ryan (Eds.). Sp ringer International Publishing, Cham, 577–594

    work page 2019

  27. [27]

    Saverio Giallorenzo, Fabrizio Montesi, and Maurizio G abbrielli. 2018. Applied Choreographies. In Formal Techniques for Distributed Objects, Compo- nents, and Systems - 38th IFIP WG 6.1 International Conferen ce, FORTE 2018, Held as Part of the 13th International Federat ed Conference on Distributed Computing Techniques, DisCoTec 2018, Madrid, Spain, June...

    work page 2018

  28. [28]

    Saverio Giallorenzo, Fabrizio Montesi, and Marco Pere ssotti. 2024. Choral: Object-oriented Choreographic Prog ramming. ACM Trans. Program. Lang. Syst. 46, 1, Article 1 (Jan. 2024), 59 pages. https://doi.org/10. 1145/3632398

    work page 2024

  29. [29]

    Jean-Yves Girard. 1987. Linear logic. Theoretical Computer Science 50, 1 (1987), 1–101. https://doi.org/10.1016/0304-3975( 87)90045-4

    work page doi:10.1016/0304-3975( 1987

  30. [30]

    Jean-Yves Girard. 1998. Light Linear Logic. Information and Computation 143, 2 (1998), 175–204. https://doi.org/10.1006/inco.19 98.2700

    work page doi:10.1006/inco.19 1998

  31. [31]

    Jean-Yves Girard, Paul Taylor, and Yves Lafont. 1989. Proofs and types . Vol. 7. Cambridge university press Cambridge

    work page 1989

  32. [32]

    Vaandrager

    Jan Friso Groote and Frits W. Vaandrager. 1992. Structu red Operational Semantics and Bisimulation as a Congruence . Inf. Comput. 100, 2 (1992), 202–260. https://doi.org/10.1016/0890-5401(92)90013- 6 Manuscript submitted to ACM 28 Acclavio et al

    work page doi:10.1016/0890-5401(92)90013- 1992

  33. [33]

    David Harel, Dexter Kozen, and Jerzy Tiuryn. 2002. Dynamic Logic . Springer Netherlands, Dordrecht, 99–217. https://doi.org/10.1007/978-94-017-0456-4_2

    work page doi:10.1007/978-94-017-0456-4_2 2002

  34. [34]

    David Harel, Amir Pnueli, and Jonathan Stavi. 1983. Pro positional dynamic logic of nonregular programs. J. Comput. System Sci. 26, 2 (1983), 222–243

    work page 1983

  35. [35]

    Harel and R

    D. Harel and R. Sherman. 1985. Propositional dynamic lo gic of flowcharts. Information and Control 64, 1 (1985), 119–135. https://doi.org/10.1016/S0019-9958(85)80047-4 Intern ational Conference on Foundations of Computation Theory

    work page doi:10.1016/s0019-9958(85)80047-4 1985

  36. [36]

    David Harel and Eli Singerman. 1996. More on nonregular PDL: Finite models and Fibonacci-like programs. information and computation 128, 2 (1996), 109–118

    work page 1996

  37. [37]

    David Hemer, Robert Colvin, Ian Hayes, and Paul Stroope r. 2002. Don’t care non-determinism in logic program refinem ent. Electronic Notes in Theoretical Computer Science 61 (2002), 101–121

    work page 2002

  38. [38]

    Brian Hill and Francesca Poggiolesi. 2010. A Contracti on-free and Cut-free Sequent Calculus for Propositional Dy namic Logic. Studia Logica 94, 1 (2010), 47–72. https://doi.org/10.1007/s11225-010-922 4-z

    work page doi:10.1007/s11225-010-922 2010

  39. [39]

    Hirsch and Deepak Garg

    Andrew K. Hirsch and Deepak Garg. 2022. Pirouette: high er-order typed functional choreographies. Proc. ACM Program. Lang. 6, POPL (2022), 1–27. https://doi.org/10.1145/3498684

    work page doi:10.1145/3498684 2022

  40. [40]

    Tony Hoare, Bernhard Möller, Georg Struth, and Ian Wehr man. 2011. Concurrent Kleene Algebra and its Foundations. J. Log. Algebraic Methods Program. 80, 6 (2011), 266–296. https://doi.org/10.1016/J.JLAP.2 011.04.005

    work page doi:10.1016/j.jlap.2 2011

  41. [41]

    Tony Hoare, Stephan van Staden, Bernhard Möller, Georg Struth, and Huibiao Zhu. 2016. Developments in concurrent K leene algebra. J. Log. Algebraic Methods Program. 85, 4 (2016), 617–636. https://doi.org/10.1016/J.JLAMP. 2015.09.012

    work page doi:10.1016/j.jlamp 2016

  42. [42]

    John E Hopcroft, Rajeev Motwani, and Jeffrey D Ullman. 20 01. Introduction to automata theory, languages, and comput ation. Acm Sigact News 32, 1 (2001), 60–65

    work page 2001

  43. [43]

    John E Hoperoft and Jeffrey D Ullman. 1979. Introduction to automata theory, languages, and computation. Addison-Welsey, NY (1979)

    work page 1979

  44. [44]

    Ross Horne, Ki Yung Ahn, Shang-wei Lin, and Alwen Tiu. 20 18. Quasi-Open Bisimilarity with Mismatch is Intuitionist ic. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Oxford, United Kingdom) (LICS ’18) . Association for Computing Machinery, New York, NY, USA, 26–35. https://doi.org/10.1145/3209108.320912 5

    work page doi:10.1145/3209108.320912

  45. [45]

    Ross Horne and Sjouke Mauw. 2021. Discovering ePasspor t Vulnerabilities using Bisimilarity. Logical Methods in Computer Science Volume 17, Issue 2, Article 24 (Jun 2021). https://doi.org/10.23638/ LMCS-17(2:24)2021

    work page 2021

  46. [46]

    Xiao Jun Chen and Rocco De Nicola. 2001. Algebraic chara cterizations of trace and decorated trace equivalences over tree-like structures. Theoretical Computer Science 254, 1 (2001), 337–361. https://doi.org/10.1016/S0304-3 975(99)00300-X

    work page doi:10.1016/s0304-3 2001

  47. [47]

    Tobias Kappé, Paul Brunet, Jurriaan Rot, Alexandra Sil va, Jana Wagemaker, and Fabio Zanasi. 2019. Kleene Algebra w ith Observations. In 30th International Conference on Concurrency Theory, CONCUR 20 19, August 27-30, 2019, Amsterdam, the Netherlands (LIPIcs, Vol. 140), Wan J. Fokkink and Rob van Glabbeek (Eds.). Schloss Dagstuhl - Leibniz-Zen trum für In...

    work page 2019

  48. [48]

    Tobias Kappé, Paul Brunet, Alexandra Silva, Jana Wagem aker, and Fabio Zanasi. 2020. Concurrent Kleene Algebra wit h Observations: From Hypotheses to Completeness. In Foundations of Software Science and Computation Structure s - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice o f Software,...

    work page doi:10.1007/978-3-030-45231-5_ 2020

  49. [49]

    Dexter Kozen. 1996. Kleene algebra with tests and commu tativity conditions. In Tools and Algorithms for the Construction and Analysis of Sy stems, Tiziana Margaria and Bernhard Steffen (Eds.). Springer Berl in Heidelberg, Berlin, Heidelberg, 14–33

    work page 1996

  50. [50]

    Dexter Kozen. 1997. Kleene Algebra with Tests. ACM Trans. Program. Lang. Syst. 19, 3 (1997), 427–443. https://doi.org/10.1145/256167.2 56195

    work page doi:10.1145/256167.2 1997

  51. [51]

    Dexter Kozen and Rohit Parikh. 1981. An elementary proo f of the completeness of PDL. Theoretical Computer Science 14, 1 (1981), 113–118. https://doi.org/10.1016/0304-3975(81)90019-0

    work page doi:10.1016/0304-3975(81)90019-0 1981

  52. [52]

    Dexter C Kozen. 2007. Automata and computability. Springer Science & Business Media

    work page 2007

  53. [53]

    Yves Lafont. 2004. Soft linear logic and polynomial tim e. Theoretical computer science 318, 1-2 (2004), 163–180

    work page 2004

  54. [54]

    Martin Lange. 2003. Games for modal and temporal logics . (2003)

    work page 2003

  55. [55]

    Chuck Liang and Dale Miller. 2021. Focusing Gentzen’s L K proof system. (Nov. 2021). https://hal.science/hal-034 57379 working paper or preprint

    work page 2021

  56. [56]

    John W Lloyd. 2012. Foundations of logic programming . Springer Science & Business Media

    work page 2012

  57. [57]

    Mayer and Larry J

    Alain J. Mayer and Larry J. Stockmeyer. 1996. The comple xity of PDL with interleaving. Theoretical Computer Science 161, 1 (1996), 109–122. https://doi.org/10.1016/0304-3975(95)00095-X

    work page doi:10.1016/0304-3975(95)00095-x 1996

  58. [58]

    Damiano Mazza. 2006. Linear logic and polynomial time. Mathematical Structures in Computer Science 16, 6 (2006), 947–988. https://doi.org/10.1017/S0960129506005688

    work page doi:10.1017/s0960129506005688 2006

  59. [59]

    Damiano Mazza. 2015. Simple Parsimonious Types and Log arithmic Space. In 24th EACSL Annual Conference on Computer Science Logic, CSL 2015 (LIPIcs, Vol. 41). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 24–40 . https://doi.org/10.4230/LIPIcs.CSL.2015.24

    work page doi:10.4230/lipics.csl.2015.24 2015

  60. [60]

    Damiano Mazza and Kazushige Terui. 2015. Parsimonious Types and Non-uniform Computation. In Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6 -10, 2015, Proceedings, Part II (Lecture Notes in Computer Sci ence, Vol. 9135) , Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Spe ckmann (Eds...

    work page 2015

  61. [61]

    Dale Miller, Gopalan Nadathur, Frank Pfenning, and And re Scedrov. 1991. Uniform proofs as a foundation for logic pr ogramming. Annals of Pure and Applied Logic 51, 1 (1991), 125–157. https://doi.org/10.1016/0168-007 2(91)90068-W Manuscript submitted to ACM On Propositional Dynamic Logic and Concurrency 29

    work page doi:10.1016/0168-007 1991

  62. [62]

    Robin Milner. 1980. A Calculus of Communicating Systems . Lecture Notes in Computer Science, Vol. 92. Springer. https://doi.org/10.1007/3-540-10235-3

    work page doi:10.1007/3-540-10235-3 1980

  63. [63]

    Robin Milner, Joachim Parrow, and David Walker. 1992. A calculus of mobile processes, I. Information and Computation 100, 1 (1992), 1–40. https://doi.org/10.1016/0890-5401(92)90008-4

    work page doi:10.1016/0890-5401(92)90008-4 1992

  64. [64]

    Fabrizio Montesi. 2013. Choreographic Programming . Ph.D. Thesis. IT University of Copenhagen. https://www.fabriziomontesi.com/files/choreographic- programming.pdf

    work page 2013

  65. [65]

    Fabrizio Montesi. 2023. Introduction to Choreographies. Cambridge University Press. https://doi.org/10.1017/9 781108981491

    work page doi:10.1017/9 2023

  66. [66]

    Damian Niwiński and Igor Walukiewicz. 1996. Games for t he /u1D707-calculus. Theoretical Computer Science 163, 1 (1996), 99–116. https://doi.org/10.1016/0304-3975(95)00136-0

    work page doi:10.1016/0304-3975(95)00136-0 1996

  67. [67]

    Object Management Group. 2011. Business Process Model and Notation. http://www.omg.org/spec/BPMN/2.0/

    work page 2011

  68. [68]

    Michel Parigot. 1992. /u1D706/u1D707-Calculus: An algorithmic interpretation of classical nat ural deduction. In Logic Programming and Automated Reasoning , Andrei Voronkov (Ed.). Springer Berlin Heidelberg, Berlin , Heidelberg, 190–201

    work page 1992

  69. [69]

    David Peleg. 1987. Communication in concurrent dynami c logic. J. Comput. System Sci. 35, 1 (1987), 23–58. https://doi.org/10.1016/0022-0000(87)90035-3

    work page doi:10.1016/0022-0000(87)90035-3 1987

  70. [70]

    David Peleg. 1987. Concurrent dynamic logic. J. ACM 34, 2 (apr 1987), 450–479. https://doi.org/10.1145/23005 .23008

    work page doi:10.1145/23005 1987

  71. [71]

    David Peleg. 1987. Concurrent dynamic logic. J. ACM 34, 2 (April 1987), 450–479. https://doi.org/10.1145/230 05.23008

    work page doi:10.1145/230 1987

  72. [72]

    David Peleg. 1987. Concurrent program schemes and thei r logics. Theoretical Computer Science 55, 1 (1987), 1–45. https://doi.org/10.1016/0304-3975(87)90088-0

    work page doi:10.1016/0304-3975(87)90088-0 1987

  73. [73]

    V. R. Pratt. 1982. Using graphs to understand PDL. In Logics of Programs , Dexter Kozen (Ed.). Springer Berlin Heidelberg, Berlin, H eidelberg, 387–396

    work page 1982

  74. [74]

    Davide Sangiorgi and David Walker. 2001. The Pi-Calculus - a theory of mobile processes . Cambridge University Press

    work page 2001

  75. [75]

    Todd Schmid, Tobias Kappé, and Alexandra Silva. 2023. A Complete Inference System for Skip-free Guarded Kleene Alg ebra with Tests. In Pro- gramming Languages and Systems - 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-2 7, 2023, Pro...

    work page doi:10.1007/978-3-031- 2023

  76. [76]

    Gan Shen, Shun Kashiwa, and Lindsey Kuper. 2023. HasCho r: Functional Choreographic Programming for All (Function al Pearl). Proc. ACM Program. Lang. 7, ICFP (2023), 541–565. https://doi.org/10.1145/360784 9

    work page doi:10.1145/360784 2023

  77. [77]

    Alex K Simpson. 1994. The proof theory and semantics of i ntuitionistic modal logic. (1994)

    work page 1994

  78. [78]

    Colin Stirling and David Walker. 1991. Local model chec king in the modal mu-calculus. Theoretical Computer Science 89, 1 (1991), 161–177

    work page 1991

  79. [79]

    Thomas Studer. 2008. On the Proof Theory of the Modal mu- Calculus. Studia Logica: An International Journal for Symbolic Logic 89, 3 (2008), 343–363. http://www.jstor.org/stable/40268983

    work page arXiv 2008

  80. [80]

    A. S. Troelstra and H. Schwichtenberg. 2000. Basic Proof Theory (2 ed.). Cambridge University Press. https://doi.org/10. 1017/CBO9781139168717

    work page 2000

Showing first 80 references.