Pith. sign in

REVIEW 3 major objections 5 minor 44 references

The far side of the cube

T0 review · 3 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The author argues that the far side of the Abramsky cube—game semantics with every combinatorial constraint relaxed—remains a Cartesian closed, definable model of PCF extended with state and concurrency.

desk verdict A well-written didactic construction of an unrestricted game model, but the Sec. 4 definability transfer is asserted, not proved, and needs referee scrutiny. read the letter →

arxiv 1908.04291 v1 pith:C3Z3TA4V submitted 2019-08-10 cs.LO cs.PL

Dan R. Ghica This is my paper · ORCID
classification cs.LOcs.PL MSC 03B4068Q55
keywords gamesemanticsAbramskycubedefinabilityfullabstractionPCFnominalsetsconcurrencysaturation
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Game-semantic models of programming languages are usually obtained by imposing combinatorial restrictions on plays—innocence, bracketing, alternation, determinism—and each restriction is associated with a language feature such as state, control, nondeterminism, or concurrency. This paper considers the opposite extreme: what model remains when all of these restrictions are dropped, keeping only the causal requirement that every move be properly justified. The answer it argues for is that the unrestricted model is still a Cartesian closed category of strategies, once strategies are saturated by a permutative-closure construction, and that a PCF-style language extended with local state, semaphores, and a dynamic concurrency primitive can define every strategy in it. If this is right, the familiar constrained models are not separate structures but inhabited regions of a single most-general model, which also serves as an elementary entry point to game semantics.

What carries the argument

The technical engine is a nominal presentation of pointer sequences: each move occurrence carries a fresh pointer name and a justification pointer to an earlier enabling move, and plays are those pointer sequences whose justifications respect the arena's enabling relation. Strategies are prefix-closed, O-closed, equivariant sets of plays, given either as sets or as next-move functions. Composition is defined through interaction, iteration, and hiding, with deletion and hereditary justification as the two auxiliary operations. The structural surprise that carries the argument is that the copy-cat strategy $\kappa_A$ is idempotent but not a unit for composition, so the category is repaired by the Karoubi envelope: morphisms are saturated strategies of the form $\kappa_A;\sigma;\kappa_B$, and saturation adds exactly the permutative-asynchronous behaviours that make the model extensional while preserving Cartesian closure.

What would settle it

Find a saturated strategy that no term of PCF with state, semaphores, and $\sigma_{\mathrm{run}}$ can denote—for instance, a strategy whose saturation forces a P-move to occur after the initial question is answered in an order that the thread-killing reconstruction cannot hide, or one that requires an unbounded number of live threads that $\sigma_{\mathrm{run}}$ cannot simulate. Such a strategy would refute the claimed definability; alternatively, a fully worked-out proof that the ICA definability construction goes through with $\sigma_{\mathrm{run}}$ would confirm the central claim.

Watch

Extended reading notes

Core claim

The paper's central claim is that the far side of the Abramsky cube—the model reached by relaxing all four combinatorial constraints while retaining proper justification of moves—is the most general game model, a universe in which the standard PCF, Idealised-Algol, control, nondeterminism, and concurrency models all live as special cases. The development shows that strategies over arenas, presented as nominal pointer sequences, form a category under composition, and that the natural copy-cat strategy is idempotent but not a two-sided identity. Applying the Karoubi envelope construction to copy-cat yields saturated strategies, and with saturation the category is Cartesian closed and extensional: two strategies are observationally equivalent exactly when their saturations are equal. The model interprets call-by-name PCF, and definability is restored by extending the syntax with local state, local split binary semaphores, and a dynamic concurrency constant $\sigma_{\mathrm{run}}$ that lets an argument finish after the initial question has been answered; with this change, the paper states, the definability procedure for concurrent Idealised Algol can be replicated, giving a complete syntax for the model.

Load-bearing premise

The load-bearing premise is the unproved claim that the definability procedure for concurrent Idealised Algol can be replicated in the far-side model with the dynamic concurrency constant $\sigma_{\mathrm{run}}$ replacing the fork-join strategy; the paper states this in a few lines, gives no detailed proof, and explicitly calls the resulting reconstruction artificial, so if the replication fails the claimed completeness of the syntax collapses.

Editorial extensions

If this is right

  • All the usual call-by-name game models become special cases obtained by re-imposing one or more of the relaxed constraints, so semantic results about the far-side model apply immediately to the whole cube.
  • The proposed PCF extension with state, semaphores, and dynamic concurrency is fully abstract for the saturated model, meaning every strategy is denoted by some term and observationally equivalent terms get equal denotations.
  • The model is extensional rather than intensional, so reasoning about programs can be done directly on saturated strategies without quotienting by test contexts.
  • Saturation gives a rational reconstruction of the permutative saturation condition used in asynchronous game semantics, connecting the model to the semantics of asynchronous circuits and delay-insensitive systems.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial inference: if the definability transfer really goes through, the cube's constraints are best understood as definability filters—each language feature simply allows more plays—rather than as axioms that build new semantic universes; the far side is then the natural ambient category for all of them.
  • Editorial inference: a detailed, proof-level reconstruction of the ICA definability argument with $\sigma_{\mathrm{run}}$ is the obvious next step; the paper asserts the replication without giving it, so a worked-out construction would either confirm completeness or expose a missing syntactic primitive.
  • Editorial inference: because the paper notes that catch is defined only via an artificial, thread-killing reconstruction under an angelic view of divergence, a natural extension is to add explicit divergence information to the model and ask whether the far side then distinguishes angelic from demonic nondeterminism.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper proposes a game-semantic model for call-by-name simply-typed languages obtained by relaxing all the usual combinatorial constraints of the Abramsky cube (innocence, bracketing, alternation, determinism) while retaining only proper justification and the strategy closure conditions of prefix-closure, O-closure, and equivariance. Because the naive copy-cat is not a unit for composition, the author passes to the Karoubi envelope of a category of strategies, obtaining 'saturated' strategies, and claims this category is Cartesian closed. The paper further claims that a PCF-style language extended with state, semaphores, and a dynamic concurrency operator σrun is definable for this model, by transferring the ICA definability procedure of Ghica and Murawski. The exposition is largely didactic, developing arenas, plays, strategies, composition, iteration, and saturation with many worked examples.

Significance. If the central claims are established, the paper would provide a useful 'ur-model' for call-by-name game semantics: a single Cartesian closed category containing strategies for nondeterminism, state, control, and concurrency, with saturation as the only added closure principle. The nominal style with explicit pointer names is a pedagogical strength, as are the concrete strategies for arithmetic, non-determinism, state, control, and concurrency. The paper is also commendably candid about its own limitations, explicitly flagging that the definability reconstruction is 'artificial' and that several proofs are only sketched. However, the manuscript's most important technical contribution, the definability transfer in Section 4, is not actually proved, and the category-theoretic structure is only partially verified. The paper is therefore best regarded as a promising research announcement or tutorial rather than a complete proof of the advertised results.

major comments (3)
  1. [Section 4, 'Definability'; Proposition 37] The claim that 'the definability procedure for ICA can be replicated' with σrun replacing σpar is load-bearing for the paper's main advertised result, but it is asserted without proof. The paper itself notes the one difference it sees: ICA strategies are characterized by their complete plays, whereas saturated strategies in this model are not, and then states in a single sentence that the ICA definability argument 'does not make use of it.' No specific lemma of the ICA proof is cited or reproduced, and no explanation is given for how the 'kill by divergence' mechanism interacts with saturation. In particular, the paper does not show that the divergence-hiding construction yields a term whose denotation has the same saturation as the target strategy; Proposition 37 would make such an observational-equivalence argument sufficient, but no such argument is supplied. Without this step, the paper establishes only a model of PCF with certain constants, not a complete syntax for the saturated model.
  2. [Section 3.1.1, Proposition 28 (Associativity)] The proof of associativity is not rigorous as written and contains apparent errors. In Equation (1), the expression '(!C((!Bσ || AB,BC ⇂B)' appears to be missing an operand, and the subscript 'CS' is undefined. Equations (3) and (4) rely on claims that are not obvious for the pointer-sequence operations involved: that σ⇂C = σ when σ contains no C-moves, and that ⇂C 'distributes over concatenation' in the presence of iteration and hereditary justification. The proof also cites 'Prop. 5' and 'Prop. 8' where the numbering does not match the propositions being invoked. Since associativity is a basic requirement for the category, this needs either a complete, corrected proof or a precise reference to a formalized version.
  3. [Section 3.1.3, Proposition 35 (Cartesian closed structure)] The verification of Cartesian closure is incomplete. The proof leaves the exponential transpose as 'an exercise to the reader,' stating only that the re-tagging is 'induced by the two isomorphic ways in which the coproduct can associate.' The paper does not verify naturality of the transpose, the β and η equations, or the universal property of evaluation. Because the claim that the category models the simply typed lambda calculus depends on these equations, the paper needs either a full proof or a citation to a source where the details are worked out.
minor comments (5)
  1. [Section 2.2.3, State] The next-move clause for writes reads 'ˆσnew(p·wra⟨b⟩) = val(n)b', but it should almost certainly be 'ok(n)b' to match the preceding sentence and the intended behavior of acknowledging a write.
  2. [Definition 23, Iteration] The definition begins 'Given a set of pointer sequences σ∈ JM'; since σ is a set, it should be 'σ⊆JM'.
  3. [Section 3.1.1, Proposition 28] The proof references 'Prop. 5', 'Prop. 8', and 'Prop. 9' inside the associativity argument, but these labels do not correspond to the propositions in the paper; the numbering appears to be from an earlier draft.
  4. [Section 4, Definability] The phrase 'the reconstruction of catch creates a large number of concurrent threads, killing off those plays that evolve in an undesirable direction by introducing divergences, which are subsequently hidden by the angelic notion of observation' is vague; since this is the proposed mechanism behind the definability transfer, it deserves a formal description or at least an illustrative example.
  5. [Title and Abstract] The claim that the model is 'the most general game model, in which all the other game models live' is not formalized: the paper never defines a notion of embedding or inclusion between game models, so the reader cannot verify in what precise sense other models 'live' in this one.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the far-side model is constructed self-containedly; the Sec. 4 definability transfer is an unproved gap, not a circular reduction.

full rationale

This is an honest non-finding. The paper's technical derivation, comprising strategies as equivariant prefix-closed and O-closed sets of justified plays, composition via interaction/iteration/hiding, the Karoubi-envelope saturation that repairs the failure of copy-cat as identity, and the Cartesian closed structure, is carried out self-containedly in Secs. 2-3. The 'most general game model' label in the abstract is a framing premise, not a theorem: it describes the choice to relax the Abramsky-cube constraints, and Sec. 5 candidly notes that saturation is an added closure condition rather than a consequence of the cube. The only load-bearing but unproved step is in Sec. 4, where the paper says 'With this rather minor change, the definability procedure for ICA can be replicated, giving us a complete syntax for the model.' This transfers the Ghica-Murawski (2008) definability theorem by analogy while explicitly acknowledging the only difference between the two models, namely complete-play characterization, and asserting without proof that the ICA argument does not use it. That is an omitted proof or correctness risk, not circularity: the ICA theorem is an independent, parameter-free result whose stated assumptions do not include the far-side model, and the far-side syntax is not defined in terms of the claimed definability conclusion. The self-citations to Gabbay-Ghica (2012) for the nominal presentation and to Ghica-Murawski (2008) for saturation are used as established tools, not as the target of the derivation. No step reduces to its inputs by construction, so the circularity score is 0.

Assumptions & free parameters 0 free parameters · 7 assumptions · 0 invented entities

No numeric parameters are fitted; this is a qualitative mathematical construction. The design choices are captured as domain assumptions and two ad hoc choices: saturation via the Karoubi envelope and the transfer of the ICA definability argument.

assumptions (7)
  • domain assumption The enabling relation of an arena is a DAG and satisfies (e1)-(e3); therefore in A⇒B no A-move enables a B-move.
    Used in Props. 16, 19 and in the composition/hiding argument (§2.3).
  • domain assumption Pointer names are globally fresh and strategies are equivariant under name permutation.
    Needed for iteration, composition and saturation; the paper notes this is an exception to normal scoped-name models (§2.1).
  • domain assumption The language is restricted to call-by-name evaluation and simple types (base types and functions).
    Stated in §2.1; the model may not extend to call-by-value or richer type systems without changes.
  • ad hoc to paper Saturation (permutative asynchronous closure) is imposed as a closure property via the Karoubi envelope so that copycat is the identity.
    The paper itself notes saturation could be stipulated (as in Ghica-Murawski 2008) and is introduced to fix the identity law (§3.1.2, §5).
  • ad hoc to paper Proper justification is the only structural constraint retained; all other cube constraints are dropped.
    This is the 'far side' design decision; no proof establishes it as the unique maximally permissive game model (§2.1, §5).
  • ad hoc to paper The ICA definability construction transfers to the unrestricted model when the fork-join strategy σpar is replaced by σrun.
    Asserted without proof in §4; the paper acknowledges the reconstruction is artificial.
  • standard math Background in nominal sets, category theory, and the Karoubi envelope is assumed.
    Used throughout; these are established mathematical frameworks cited in the paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of The far side of the cube." pith.science (2026). https://pith.science/paper/C3Z3TA4V

@misc{pith2026190804291,
  author       = {Pith},
  title        = {Pith review of: The far side of the cube},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/C3Z3TA4V}},
  note         = {Machine review of arXiv:1908.04291}
}
read the original abstract

Game-semantic models usually start from the core model of the prototypical language PCF, which is characterised by a range of combinatorial constraints on the shape of plays. Relaxing each such constraint usually corresponds to the introduction of a new language operation, a feature of game semantics commonly known as the `Abramsky Cube'. In this presentation we relax all such combinatorial constraints, resulting in the most general game model, in which all the other game models live. This is perhaps the simplest set up in which to understand game semantics, so it should serve as a portal to the other, more complex, game models in the literature. It might also be interesting in its own right, as an extremal instance of the game-semantic paradigm.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

44 extracted references · 27 canonical work pages

  1. [1]

    Abramsky and G

    S. Abramsky and G. McCusker. Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expressions. Electr. Notes Theor. Comput. Sci., 3: 0 2--14, 1996. doi:10.1016/S1571-0661(05)80398-6. Also appeared in o2013algol

    doi:10.1016/s1571-0661(05)80398-6 1996

  2. [2]

    Abramsky and G

    S. Abramsky and G. McCusker. Game semantics. In U. Berger and H. Schwichtenberg, editors, Computational Logic, pages 1--55, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg. ISBN 978-3-642-58622-4. doi:10.1007/978-3-642-58622-4_1

    work page doi:10.1007/978-3-642-58622-4_1 1999

  3. [3]

    Introduction to Categories and Categorical Logic

    S. Abramsky and N. Tzevelekos. Introduction to categories and categorical logic. arXiv:1102.1313, February 2011. URL https://arxiv.org/abs/1102.1313

    work page Pith review arXiv 2011

  4. [4]

    Abramsky, R

    S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF . Inf. Comput., 163 0 (2): 0 409--470, 2000. doi:10.1006/inco.2000.2930

    arXiv 2000

  5. [5]

    J. C. Baez and M. Stay. Physics, topology, logic and computation: A rosetta stone. arXiv:0903.0340, March 2009. URL https://arxiv.org/abs/0903.0340. New Structures for Physics, ed. Bob Coecke, Lecture Notes in Physics vol. 813, Springer, Berlin, 2011, pp. 95-174

    work page Pith review arXiv 2009

  6. [6]

    Balmer and M

    P. Balmer and M. Schlichting. Idempotent completion of triangulated categories. Journal of Algebra, 236 0 (2): 0 819 -- 834, 2001. ISSN 0021-8693. doi:https://doi.org/10.1006/jabr.2000.8529

    work page arXiv 2001

  7. [7]

    S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. J. ACM , 31 0 (3): 0 560--599, 1984. doi:10.1145/828.833. URL https://doi.org/10.1145/828.833

    doi:10.1145/828.833 1984

  8. [8]

    Castellan, P

    S. Castellan, P. Clairambault, S. Rideau, and G. Winskel. Games and Strategies as Event Structures . Logical Methods in Computer Science , Volume 13, Issue 3 , Sept. 2017. doi:10.23638/LMCS-13(3:35)2017

    work page doi:10.23638/lmcs-13(3:35)2017 2017

Show all 44 references
  1. [9]

    Danos and R

    V. Danos and R. Harmer. Probabilistic game semantics. In 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, California, USA, June 26-29, 2000 , pages 204--213, 2000. doi:10.1109/LICS.2000.855770

  2. [10]

    Danos and R

    V. Danos and R. Harmer. The anatomy of innocence. In Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings , pages 188--202, 2001. doi:10.1007/3-540-44802-0\_14

    2001 doi

  3. [11]

    Dreyer, G

    D. Dreyer, G. Neis, and L. Birkedal. The impact of higher-order state and control effects on local relational reasoning. J. Funct. Program., 22 0 (4-5): 0 477--528, 2012. doi:10.1017/S095679681200024X. URL https://doi.org/10.1017/S095679681200024X

    2012 doi

  4. [12]

    Gabbay and D

    M. Gabbay and D. R. Ghica. Game semantics in the nominal model. Electr. Notes Theor. Comput. Sci., 286: 0 173--189, 2012. doi:10.1016/j.entcs.2012.08.012

    2012 doi

  5. [13]

    M. J. Gabbay, D. R. Ghica, and D. Petrisan. Leaving the nest: Nominal techniques for variables with interleaving scopes. In 24th EACSL Annual Conference on Computer Science Logic CSL , September 7-10, 2015, Berlin, Germany , pages 374--389, 2015. doi:10.4230/LIPIcs.CSL.2015.374

    2015 doi

  6. [14]

    D. R. Ghica. Slot games: a quantitative model of computation. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005 , pages 85--97, 2005. doi:10.1145/1040305.1040313

    2005

  7. [15]

    D. R. Ghica. Geometry of synthesis: a structured approach to VLSI design. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007 , pages 363--375, 2007. doi:10.1145/1190216.1190269

    2007

  8. [16]

    D. R. Ghica. Applications of game semantics: From program analysis to hardware synthesis. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA , pages 17--26, 2009. doi:10.1109/LICS.2009.26

    2009 doi

  9. [17]

    D. R. Ghica and A. S. Murawski. Angelic semantics of fine-grained concurrency. Ann. Pure Appl. Logic, 151 0 (2-3): 0 89--114, 2008. doi:10.1016/j.apal.2007.10.005

    2008 doi

  10. [18]

    D. R. Ghica and N. Tzevelekos. A system-level game semantics. Electr. Notes Theor. Comput. Sci., 286: 0 191--211, 2012. doi:10.1016/j.entcs.2012.08.013

    2012 doi

  11. [19]

    D. R. Ghica, K. Muroya, and T. W. Ambridge. Local reasoning for robust observational equivalence. CoRR, abs/1907.01257, 2019. URL http://arxiv.org/abs/1907.01257

    1907 arXiv

  12. [20]

    Harmer and O

    R. Harmer and O. Laurent. The anatomy of innocence revisited. In FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings , pages 224--235, 2006. doi:10.1007/11944836\_22

    2006 doi

  13. [21]

    Harmer and G

    R. Harmer and G. McCusker. A fully abstract game semantics for finite nondeterminism. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999 , pages 422--430, 1999. doi:10.1109/LICS.1999.782637

    1999

  14. [22]

    Harmer, M

    R. Harmer, M. Hyland, and P. Melli \` e s. Categorical combinatorics for innocent strategies. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings , pages 379--388, 2007. doi:10.1109/LICS.2007.14

    2007 doi

  15. [23]

    C. A. R. Hoare. Communicating sequential processes. In The origin of concurrent programming, pages 413--443. Springer, 1978

    1978

  16. [24]

    J. M. E. Hyland and C. L. Ong. On full abstraction for PCF: I , II , and III . Inf. Comput., 163 0 (2): 0 285--408, 2000. doi:10.1006/inco.2000.2917

    2000

  17. [25]

    Jeffrey and J

    A. Jeffrey and J. Rathke. Java Jr : Fully abstract trace semantics for a core java language. In Programming Languages and Systems, 14th European Symposium on Programming, ESOP 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, pages 423--438, 2005. doi:10.1007/978-3-540-31987-0\_29

    2005 doi

  18. [26]

    J. Laird. Full abstraction for functional languages with control. In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997 , pages 58--67, 1997. doi:10.1109/LICS.1997.614931

    1997

  19. [27]

    J. Laird. A game semantics of the asynchronous pi-calculus. In Concurrency Theory, 16th International Conference, San Francisco, CA, USA, August 23-26, 2005, pages 51--65, 2005. doi:10.1007/11539452\_8

    2005 doi

  20. [28]

    Lambek and P

    J. Lambek and P. J. Scott. Introduction to higher-order categorical logic, volume 7. Cambridge University Press, 1988

    1988

  21. [29]

    P. J. Landin. The next 700 programming languages. Commun. ACM , 9 0 (3): 0 157--166, 1966. doi:10.1145/365230.365257

    1966

  22. [30]

    F. W. Lawvere. Adjointness in foundations. Dialectica, 23 0 (3-4): 0 281--296, 1969. doi:10.1111/j.1746-8361.1969.tb01194.x

    1969

  23. [31]

    R. Loader. Finitary PCF is not decidable. Theor. Comput. Sci., 266 0 (1-2): 0 341--364, 2001. doi:10.1016/S0304-3975(00)00194-8

    2001 doi

  24. [32]

    Milewski

    B. Milewski. Category Theory for Programmers. Blurb, 2018

    2018

  25. [33]

    R. Milner. Fully abstract models of typed lambda-calculi. Theor. Comput. Sci., 4 0 (1): 0 1--22, 1977. doi:10.1016/0304-3975(77)90053-6

    1977 doi

  26. [34]

    A. S. Murawski and N. Tzevelekos. Nominal game semantics. Foundations and Trends in Programming Languages, 2 0 (4): 0 191--269, 2016. doi:10.1561/2500000017

    2016 doi

  27. [35]

    O'Hearn and R

    P. O'Hearn and R. Tennent. ALGOL -like Languages . Birkh\"auser, 1997

    1997

  28. [36]

    P. W. O'Hearn, J. Power, M. Takeyama, and R. D. Tennent. Syntactic control of interference revisited. Theor. Comput. Sci., 228 0 (1-2): 0 211--252, 1999. doi:10.1016/S0304-3975(98)00359-4

    1999 doi

  29. [37]

    F. Oles. Type algebras, functor categories, and block structure. DAIMI Report Series, 12 0 (156), Jan. 1983. doi:10.7146/dpb.v12i156.7430. A version appeared in o2013algol

    1983 doi

  30. [38]

    A. M. Pitts. Nominal sets: Names and symmetry in computer science, volume 57. Cambridge University Press, 2013

    2013

  31. [39]

    G. D. Plotkin. LCF considered as a programming language. Theor. Comput. Sci., 5 0 (3): 0 223--255, 1977. doi:10.1016/0304-3975(77)90044-5

    1977 doi

  32. [40]

    U. S. Reddy. Global state considered unnecessary: An introduction to object-based semantics. Lisp and Symbolic Computation, 9 0 (1): 0 7--76, 1996

    1996

  33. [41]

    J. C. Reynolds. The essence of ALGOL . In J. W. de Bakker and J. C. van Vliet, editors, Proceedings of the International Symposium on Algorithmic Languages, pages 345--372, Amsterdam, 1981. Also appeared in o2013algol

    1981

  34. [42]

    Scott and C

    D. Scott and C. Strachey. Toward a mathematical semantics for computer languages. Technical Report PRG-6, Oxford Programming Research Group, 1971

    1971

  35. [43]

    R. D. Tennent and D. R. Ghica. Abstract models of storage. Higher-Order and Symbolic Computation, 13 0 (1/2): 0 119--129, 2000. doi:10.1023/A:1010022312623

    doi

  36. [44]

    J. T. Udding. A formal model for defining and classifying delay-insensitive circuits and systems. Distributed Computing, 1 0 (4): 0 197--204, Dec 1986. ISSN 1432-0452. doi:10.1007/BF01660032

    1986 doi

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.