pith. sign in

arxiv: 2512.07240 · v2 · submitted 2025-12-08 · 💻 cs.LO

A Diagrammatic Basis for Computer Programming

Filippo Bonchi , Alessandro Di Giorgio , Elena Di Lavore This is my paper

Pith reviewed 2026-05-17 01:05 UTC · model grok-4.3

classification 💻 cs.LO
keywords tape diagramsrig categoriesimperative programmingKleene bicategoriesCartesian bicategoriesprogram semanticscategorical logic
0
0 comments X

The pith

Kleene-Cartesian rig categories let tape diagrams represent imperative programs and program logic graphically.

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

The paper defines Kleene-Cartesian rig categories as rig categories in which the tensor product carries Cartesian bicategory structure and the direct sum carries Kleene bicategory structure. It then shows that the tape diagrams for arrows in these categories supply a convenient graphical notation for imperative programs. A sympathetic reader would care because the diagrams combine parallel composition, sequential composition, iteration, and logical assertions in one visual language. This could make reasoning about stateful code and its correctness properties more direct than with conventional textual syntax.

Core claim

Kleene-Cartesian rig categories are rig categories where ⊗ forms a Cartesian bicategory while ⊕ forms a Kleene bicategory. The tape diagrams associated with such categories can conveniently deal with imperative programs and various program logic.

What carries the argument

Tape diagrams of Kleene-Cartesian rig categories, which use Cartesian bicategorical structure on ⊗ for branching and Kleene bicategorical structure on ⊕ for sequencing and fixed points.

If this is right

  • Sequential composition and iteration in programs become diagrammatic composition and Kleene-star operations.
  • State and assignment operations are expressed by the Cartesian structure on the tensor product.
  • Assertions and program logics appear as additional arrows or relations within the same diagrams.
  • Equational reasoning about program equivalence reduces to diagram rewriting.

Where Pith is reading between the lines

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

  • The same diagrammatic language might extend to model probabilistic or quantum imperative programs by replacing the rig with a suitable semiring.
  • Visual editors that manipulate these tape diagrams could serve as direct interfaces for writing and verifying low-level code.
  • Connections to existing string-diagram calculi for concurrency suggest a route toward unified graphical semantics across programming paradigms.

Load-bearing premise

Adding Cartesian bicategory structure to the tensor and Kleene bicategory structure to the sum inside a rig category is enough for the resulting tape diagrams to model imperative programs and program logic.

What would settle it

An imperative program fragment or a Hoare-triple-style assertion whose intended behavior cannot be captured by any finite tape diagram in a Kleene-Cartesian rig category would refute the claim.

Figures

Figures reproduced from arXiv: 2512.07240 by Alessandro Di Giorgio, Elena Di Lavore, Filippo Bonchi.

Figure 1
Figure 1. Figure 1: Categorical structures correspond to logics. An idea, originating at least from Bainbridge [Bai76], is to model data flow using the Cartesian product of relations, (Rel, ⊗, 1), and control flow using a different monoidal structure on relations: (Rel, ⊕, 0). In this second structure, the monoidal product ⊕ is the disjoint union of sets, which acts both as a categorical product and a coproduct, hence, a bipr… view at source ↗
Figure 2
Figure 2. Figure 2: String diagrams for the axioms of coherent (co)commutative (co)monoids in Definition 3.1.(1),(2),(3) and Definition 4.1.(1),(2),(3). The gray colouring on the labels should be instantiated to black for Definition 3.1 and to white for Definition 4.1. The coherence axioms – in last two rows – are unlabeled as they will be implicit in the graphical representation by means of tapes diagrams. for f : X → Y and … view at source ↗
Figure 3
Figure 3. Figure 3: String diagrams for the axioms of Cartesian bicategories: lax natu￾rality, special Frobenius algebras and adjointness in Definition 3.1.(4),(5),(6). (2) (◀X, !X) is a cocommutative comonoid: ◀X; (◀X ⊗idX) =◀X; (idX⊗ ◀X), ◀X; (!X ⊗ idX) = idX and ◀X; σX,X =◀X; (3) (▶X, ¡X) and (◀X, !X) are coherent with the monoidal structure: ▶1= id1 ▶X⊗Y = (idX ⊗ σY,X ⊗ idY ); (▶X ⊗ ▶Y ) ¡1 = id1 ¡X⊗Y = ¡X ⊗ ¡Y ◀1= id1 ◀X… view at source ↗
Figure 4
Figure 4. Figure 4: String diagrams for the axioms of fb categories with idempotent convolution: naturality in Definition 4.1.(4) and adjointness in (4.2) When ⊔ is idempotent, an fb category is not only CMon-enriched but also poset￾enriched. In this case, the pair (◁X, ⊸X) forms a right adjoint to (▷X, ⊸X): idX ≥ ◁X ; ▷X, ▷X ; ◁X ≥ idX⊗X, idX ≥ ⊸X ; ⊸X, X⊸ ; ⊸X ≥ id1. (4.2) Conversely, if an fb category is poset-enriched and… view at source ↗
Figure 5
Figure 5. Figure 5: String diagrams for the axioms of traces in Kleene bicategories. Like in any finite biproduct category with trace (see e.g. [CS¸94]), in a Kleene bicategory one can define for each endomorphism f : X → X, a morphism f ∗ : X → X as on the right of (4.1). The distinguishing property of Kleene bicategories is that (·) ∗ satisfies the laws of Kleene star as axiomatised by Kozen in [Koz94]. Definition 4.8. A Kl… view at source ↗
Figure 6
Figure 6. Figure 6: Tape axioms for Kleene bicategory [PITH_FULL_IMAGE:figures/full_fig_p025_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Axioms of Cartesian bicategories 7.2. Semantics of Tape Diagrams. Recall from Section 5 that an interpretation I = (αS, αΣ) of a monoidal signature (S, Σ) in a sesquistrict rig category H : S → C consists of αS : S → Ob(S) and αΣ : Σ → Ar(C) preserving (co)arities of symbols s ∈ Σ. Whenever C is a kc-rig category, I gives rises uniquely, by freeness of KCTΣ, to a morphism of kc-rig categories J·KI : KCTΣ →… view at source ↗
Figure 8
Figure 8. Figure 8: Posetal uniformity axioms in tape diagrams [PITH_FULL_IMAGE:figures/full_fig_p026_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: The Kleene-Cartesian theory of Peano. η; β. Since η; β factors through KCTΣ,I , it obviously preserves ≤I and thus I is a model of (Σ,I). To conclude that the correspondene is bijective, it is enough to observe that J·KI = η; ˜α ♯ Σ . 8. The Kleene-Cartesian Theory of Peano In Section 7.3, we introduced kc theories and presented several illustrative examples. We now provide an additional example of a kc th… view at source ↗
Figure 10
Figure 10. Figure 10: Peano’s theory of the natural numbers. Thus, by (AU2) the inclusion below holds and the derivation concludes the proof. A (ind) ≤Q A s 0 ≤Q P A (AT1) =Q P A . The other Peano’s axioms state that 0 is a natural number, s is an injective function and that 0 is not the successor of any natural number. These are illustrated by means of tapes in [PITH_FULL_IMAGE:figures/full_fig_p030_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: String diagram axioms for symmetries. Definition A.1. A symmetric monoidal category (C, ⊙, I) is traced if it is endowed with an operator trS : C(S ⊙ X, S ⊙ Y ) → C(X, Y ), for all objects S, X and Y of C, that satisfies the axioms in Figure 12a for all suitably typed f, g, u and v. A morphism of traced monoidal categories is a symmetric monoidal functor F: B → C that preserves the trace, namely F(trSf) =… view at source ↗
Figure 12
Figure 12. Figure 12: Algebraic and string diagrammatic presentations of the trace axioms and the uniformity axiom [PITH_FULL_IMAGE:figures/full_fig_p047_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Coherence Axioms of symmetric rig categories [PITH_FULL_IMAGE:figures/full_fig_p050_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: Kleene star from trace and trace from Kleene star in finite biproduct categories. that is fST ≤ gST . Similarly for the others. Viceversa from fST ≤ gST fSY ≤ gSY fXT ≤ gXT and fXY ≤ gXY , one can use the formal form to deduce immediately that f ≤ g. The two posetal uniformity axioms enjoy alternative characterisations that will be useful later on through this appendix: If ∃r1, r2 : S → T s.t. r2 ≤ r1 and… view at source ↗
Figure 15
Figure 15. Figure 15: Equivalent uniformity axioms. Proof. The poset enirched monoidal category obtained by inverting the 2-cells also has biproducts and trace. Thus, we show the first of the implications in [PITH_FULL_IMAGE:figures/full_fig_p054_15.png] view at source ↗
Figure 14
Figure 14. Figure 14: By Corollary D.5 and Lemma D.8, (·) ∗ satisfies the laws in (4.7). Thus, it is a Kleene star. Conversely, suppose that C has a Kleene star operator (·) ∗ . One can easily show (e.g., by using completeness of Kozen axiomatisation in [Koz94]) that the laws of Kleene star in (4.7) entail those in (D.1). Thus, by Proposition D.3, (·) ∗ gives us a trace as defined in the right of [PITH_FULL_IMAGE:figures/full… view at source ↗
read the original abstract

Tape diagrams provide a convenient graphical notation for arrows of rig categories, i.e., categories equipped with two monoidal products, $\oplus$ and $\otimes$. In this work, we introduce Kleene-Cartesian rig categories, namely rig categories where $\otimes$ provides a Cartesian bicategory, while $\oplus$ a Kleene bicategory. We show that the associated tape diagrams can conveniently deal with imperative programs and various program logic.

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 / 1 minor

Summary. The paper introduces Kleene-Cartesian rig categories, which equip rig categories with a Cartesian bicategory structure on the monoidal product ⊗ and a Kleene bicategory structure on ⊕. It claims that the associated tape diagrams then provide a convenient graphical notation for modeling and reasoning about imperative programs together with various program logics.

Significance. If the compatibility between the bicategory structures and the underlying rig operations can be established, the work would supply a diagrammatic calculus for imperative constructs such as iteration and branching. This could strengthen the connection between graphical calculi and program semantics, but the significance hinges on concrete demonstrations that the diagrams preserve the intended program behavior.

major comments (1)
  1. [Definition of Kleene-Cartesian rig categories (and the subsequent tape-diagram semantics)] The central claim rests on the assumption that no additional coherence conditions are required for the Kleene fixed-point operator and Cartesian projections to distribute properly over the rig multiplication. The manuscript should supply an explicit verification or counter-example check that the combined axioms yield sound encodings of loops and assignments; without this step the modeling claim remains unproven.
minor comments (1)
  1. [Abstract] The abstract would be clearer if it briefly indicated which imperative constructs (e.g., while-loops, assignments) are directly represented by which diagram operations.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We are grateful to the referee for their insightful comments on our paper. We believe our introduction of Kleene-Cartesian rig categories provides a robust framework for diagrammatic reasoning about imperative programs, and we clarify the points raised below.

read point-by-point responses

  1. Referee: [Definition of Kleene-Cartesian rig categories (and the subsequent tape-diagram semantics)] The central claim rests on the assumption that no additional coherence conditions are required for the Kleene fixed-point operator and Cartesian projections to distribute properly over the rig multiplication. The manuscript should supply an explicit verification or counter-example check that the combined axioms yield sound encodings of loops and assignments; without this step the modeling claim remains unproven.

    Authors: The referee correctly identifies that the soundness of the tape diagram semantics for loops and assignments relies on the proper interaction between the Kleene fixed-point and the Cartesian structure via the rig operations. However, we maintain that the existing axioms in the definition of Kleene-Cartesian rig categories already ensure this compatibility without requiring additional coherence conditions. The Kleene bicategory axioms for ⊕ include the necessary fixed-point properties that are natural with respect to the monoidal structure, and the Cartesian bicategory axioms for ⊗ provide the projections that distribute appropriately over the rig multiplication by the rig category definition. In Section 3 of the manuscript, we define these structures, and in Section 4, we illustrate their use in encoding programs, showing that the diagrams correctly model iteration and branching. To address the referee's request for explicit verification, we will include a dedicated paragraph or subsection in the revised manuscript that explicitly checks the coherence for the key cases of loop and assignment encodings. revision: yes

Circularity Check

0 steps flagged

No circularity: modeling follows directly from new Kleene-Cartesian rig category definitions

full rationale

The paper defines Kleene-Cartesian rig categories by equipping rig categories with a Cartesian bicategory structure on ⊗ and a Kleene bicategory structure on ⊕. It then claims that the associated tape diagrams can model imperative programs and program logic. This is a constructive forward step from the introduced axioms and diagrammatic syntax to the claimed applications. No equations or claims reduce by construction to prior fitted quantities, self-citations, or renamed inputs; the derivation chain remains self-contained against the paper's own definitions without load-bearing circular reductions.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 1 invented entities

The abstract relies on standard definitions of rig categories and bicategories; the central novelty is the specific combination introduced for programming applications. No free parameters or invented entities beyond the new category definition are visible.

axioms (3)
  • standard math Rig categories are equipped with two monoidal products ⊕ and ⊗.
    Standard background assumption in the theory of rig categories.
  • domain assumption ⊗ forms a Cartesian bicategory.
    Required by the definition of Kleene-Cartesian rig categories.
  • domain assumption ⊕ forms a Kleene bicategory.
    Required by the definition of Kleene-Cartesian rig categories.
invented entities (1)
  • Kleene-Cartesian rig categories no independent evidence
    purpose: To support tape diagrams that represent imperative programs and program logic.
    Newly defined structure that combines the two bicategory properties.

pith-pipeline@v0.9.0 · 5356 in / 1426 out tokens · 40267 ms · 2026-05-17T01:05:00.676957+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

24 extracted references · 24 canonical work pages · 5 internal anchors

  1. [1]

    Sufficient incorrectness logic: SIL and separation SIL, 2023.arXiv:2310.18156

    [ABGL23] Flavio Ascari, Roberto Bruni, Roberta Gori, and Francesco Logozzo. Sufficient incorrectness logic: SIL and separation SIL, 2023.arXiv:2310.18156. [AK01] Allegra Angus and Dexter Kozen. Kleene algebra with tests and program schematology. Technical report, Cornell University,

    work page arXiv 2023

  2. [2]

    Tape diagrams for monoidal monads

    [BCGL25] Filippo Bonchi, Cipriano Junior Cioffo, Alessandro Di Giorgio, and Elena Di Lavore. Tape diagrams for monoidal monads. In Corina Cˆ ırstea and Alexander Knapp, editors,11th Conference on Algebra and Coalgebra in Computer Science, CALCO 2025, June 16-18, 2025, University of Strathclyde, UK, volume 342 ofLIPIcs, pages 11:1–11:24. Schloss Dagstuhl -...

    work page 2025

  3. [3]

    In: Cîrstea, C., Knapp, A

    URL:https://doi.org/10.4230/LIPIcs.CALCO.2025.11, doi:10.4230/ LIPICS.CALCO.2025.11. [BCH24] Chris Barrett, Daniel Castle, and Willem Heijltjes. The relational machine calculus. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors,Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-...

    work page doi:10.4230/lipics.calco.2025.11 2025

  4. [4]

    [BDGHS24] Filippo Bonchi, Alessandro Di Giorgio, Nathan Haydon, and Pawel Sobocinski

    URL:https://arxiv.org/abs/2410.03561,arXiv:2410.03561. [BDGHS24] Filippo Bonchi, Alessandro Di Giorgio, Nathan Haydon, and Pawel Sobocinski. Diagrammatic algebra of first order logic. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, ...

    work page arXiv 2024

  5. [5]

    doi:10.1145/3661814. 3662078. [BDGS23] Filippo Bonchi, Alessandro Di Giorgio, and Alessio Santamaria. Deconstructing the calcu- lus of relations with tape diagrams.Proceedings of the ACM on Programming Languages, 7(POPL):1864–1894,

    work page doi:10.1145/3661814

  6. [6]

    Relational Connectors and Heterogeneous Simulations

    [BGL25] Filippo Bonchi, Alessandro Di Giorgio, and Elena Di Lavore. A diagrammatic algebra for program logics. In Parosh Aziz Abdulla and Delia Kesner, editors,Foundations of Software Science and Computation Structures - 28th International Conference, FoSSaCS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETA...

    work page doi:10.1007/978-3-031-90897-2 2025

  7. [7]

    Kleene algebra with converse

    [BP14] Paul Brunet and Damien Pous. Kleene algebra with converse. InRelational and Algebraic Methods in Computer Science: 14th International Conference, RAMiCS 2014, Marienstatt, Germany, April 28–May 1,

    work page 2014

  8. [8]

    Functorial Semantics for Relational Theories

    43 [BPS17] Filippo Bonchi, Dusko Pavlovic, and Pawel Sobocinski. Functorial semantics for relational theories.arXiv preprint arXiv:1711.08699,

    work page internal anchor Pith review Pith/arXiv arXiv

  9. [9]

    Graphical Conjunctive Queries

    [BSS18] Filippo Bonchi, Jens Seeber, and Pawel Sobocinski. Graphical Conjunctive Queries. In Dan Ghica and Achim Jung, editors,27th EACSL Annual Conference on Computer Science Logic (CSL 2018), volume 119 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 13:1–13:23, Dagstuhl, Germany,

    work page 2018

  10. [10]

    doi: 10.4230/LIPIcs.CSL.2018.13

    Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. doi: 10.4230/LIPIcs.CSL.2018.13. [BSZ15] Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. Full abstraction for signal flow graphs. ACM SIGPLAN Notices, 50(1):515–526,

    work page doi:10.4230/lipics.csl.2018.13 2018

  11. [11]

    Automatic inference of necessary preconditions

    [CCFL13] Patrick Cousot, Radhia Cousot, Manuel F¨ ahndrich, and Francesco Logozzo. Automatic inference of necessary preconditions. In Roberto Giacobazzi, Josh Berdine, and Isabella Mastroeni, editors,Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22,

    work page 2013

  12. [12]

    Springer, 2013.doi:10.1007/978-3-642-35873-9\_10

    Proceedings, volume 7737 ofLecture Notes in Computer Science, pages 128–148. Springer, 2013.doi:10.1007/978-3-642-35873-9\_10. [CD11] Bob Coecke and Ross Duncan. Interacting quantum observables: categorical algebra and diagrammatics.New Journal of Physics, 13(4):043016,

    work page doi:10.1007/978-3-642-35873-9 2013

  13. [13]

    Sheet diagrams for bimonoidal categories, 2020.arXiv:2010.13361

    [CDH20] Cole Comfort, Antonin Delpeuch, and Jules Hedges. Sheet diagrams for bimonoidal categories, 2020.arXiv:2010.13361. [CG99] Andrea Corradini and Fabio Gadducci. An algebraic presentation of term graphs, via gs-monoidal categories.Applied Categorical Structures, 7(4):299–331,

    work page arXiv 2020

  14. [14]

    Two Roads to Classicality

    arXiv:1701.07400,doi:10.4204/EPTCS.266.7. [CW87] Aurelio Carboni and R. F. C. Walters. Cartesian bicategories I.Journal of Pure and Applied Algebra, 49:11–32,

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.4204/eptcs.266.7

  15. [15]

    A presentation of the category of stochastic matrices

    doi:10.1080/00927877608822127. [Fri09] Tobias Fritz. A presentation of the category of stochastic matrices.CoRR, abs/0902.2554,

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.1080/00927877608822127

  16. [16]

    String diagrams for regular logic (extended abstract)

    [FS20] Brendan Fong and David Spivak. String diagrams for regular logic (extended abstract). In John Baez and Bob Coecke, editors,Applied Category Theory 2019, volume 323 ofElectronic Proceedings in Theoretical Computer Science, page 196–229. Open Publishing Association, Sep 2020.doi:10.4204/eptcs.323.14. [GJ16] Dan R. Ghica and Achim Jung. Categorical se...

    work page doi:10.4204/eptcs.323.14 2019

  17. [17]

    Props in Network Theory

    [JCB17] Franciscus Rebro John C. Baez, Brandon Coya. Props in network theory.CoRR, abs/1707.08321,

    work page internal anchor Pith review Pith/arXiv arXiv

  18. [18]

    Props in Network Theory

    URL:http://arxiv.org/abs/1707.08321,arXiv:1707.08321. [JS91] Andr´ e Joyal and Ross Street. The geometry of tensor calculus, I.Advances in Mathematics, 88(1):55–112, July 1991.doi:10.1016/0001-8708(91)90003-P. [JSV96a] Andr´ e Joyal, Ross Street, and Dominic Verity. Traced monoidal categories.Math Procs Cambridge Philosophical Society, 119(3):447–468, 4

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.1016/0001-8708(91)90003-p 1991

  19. [19]

    [Law63] F

    Springer.doi:10.1007/BFb0059555. [Law63] F. W. Lawvere.Functorial Semantics of Algebraic Theories. PhD thesis, Columbia University, New York, NY, USA,

    work page doi:10.1007/bfb0059555

  20. [20]

    Thirty-seven years of relational hoare logic: remarks on its principles and history

    [Nau20] David A Naumann. Thirty-seven years of relational hoare logic: remarks on its principles and history. InLeveraging Applications of Formal Methods, Verification and Validation: Engineering Principles: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part II 9, pa...

    work page 2020

  21. [21]

    On the positive calculus of relations with transitive closure

    [Pou18] Damien Pous. On the positive calculus of relations with transitive closure. In Rolf Niedermeier and Brigitte Vall´ ee, editors,35th Symposium on Theoretical Aspects of Computer Science, STACS 2018, February 28 to March 3, 2018, Caen, France, volume 96 ofLIPIcs, pages 3:1–3:16. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik, 2018.doi:10.4230/L...

    work page doi:10.4230/lipics.stacs.2018.3 2018

  22. [22]

    [Pra76] Vaughan R Pratt

    doi:10.1017/S0960129597002375. [Pra76] Vaughan R Pratt. Semantical considerations on floyd-hoare logic. In17th Annual Symposium on Foundations of Computer Science (sfcs 1976), pages 109–121. IEEE,

    work page doi:10.1017/s0960129597002375 1976

  23. [23]

    [SD16] Marcelo Sousa and Isil Dillig

    doi:10.46298/lmcs-19(1:13)2023. [SD16] Marcelo Sousa and Isil Dillig. Cartesian hoare logic for verifying k-safety properties. InProceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 57–69,

    work page doi:10.46298/lmcs-19(1:13)2023 2023

  24. [24]

    Quantum relational hoare logic.Proc

    [Unr19] Dominique Unruh. Quantum relational hoare logic.Proc. ACM Program. Lang., 3(POPL), January 2019.doi:10.1145/3290346. [Win93] Glynn Winskel.The formal semantics of programming languages: an introduction. MIT press,

    work page doi:10.1145/3290346 2019