Pith. sign in

REVIEW 2 major objections 3 minor 41 references

Big Steps in Higher-Order Mathematical Operational Semantics

T0 review · 2 major / 3 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read A categorical proof now establishes when small-step and big-step operational semantics coincide.

desk verdict The main theorem is real and likely correct, but the paper never closes the gap between its omega-continuous monad hypothesis and the deterministic examples run with T = Id. read the letter →

arxiv 2506.01076 v2 pith:ZKI6TTRI submitted 2025-06-01 cs.LO

Sergey Goncharov , Pouya Partow , Stelios Tsampas This is my paper
classification cs.LO MSC 68Q5518C1503B40
keywords operationalsemanticsbig-stepsmall-stephigher-orderabstractGSOScategorytheorymonadslambdacalculuscoalgebra
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

This paper claims that the standard equivalence between small-step and big-step operational semantics — a program evaluates to a value exactly when it can be reduced to that value in many small steps — can be proven once, at a high level of abstraction, instead of being re-proven for each programming language. It introduces a categorical notion of big-step SOS alongside the existing higher-order abstract GSOS framework, and shows that from any small-step specification satisfying a condition called strong separation one can automatically derive an equivalent big-step specification. If correct, this gives a single theorem covering typed combinatory logic, recursion and conditionals, nondeterminism and parallelism, call-by-value evaluation with auxiliary operators, and the call-by-name $\lambda$ calculus with binders. The argument works by splitting syntax into values and computations, and by using $\omega$-continuous monads so that recursive evaluation can be expressed as a least fixed point.

What carries the argument

The machinery is four interlocking categorical objects. (1) A separated abstract HO-GSOS law partitions the signature into value formers $\Sigma_v$ and computation formers $\Sigma_c$, and the behaviour into a value-behaviour part $D$ and a computation part given by a strong monad $T$; this makes the object of closed terms decompose into values plus computations and lets multi-step transitions be defined over the computation part. (2) Strong separation (Definition 3.6) is a commutativity condition on the computation-rule transformation $\rho_c$: it requires that rules with at least one computation premise have the conclusion shape of a patience rule, so that evaluation is transparent to internal reductions. (3) $\omega$-continuous monads and $\omega$-continuous distributive laws $\chi$ supply least fixed points, so both the multi-step semantics $\hat{\beta}$ and the big-step semantics $\hat{\zeta}$ are defined as Kleene fixpoints. (4) The translation (17) converts a separated small-step law into an abstract big-step SOS law $\xi$, and Theorem 5.4 proves the two resulting fixed-point semantics coincide on computations.

What would settle it

Take the call-by-value specification from Section 6.4 rewritten with auxiliary operators, and compute both the multi-step semantics $\hat{\beta}$ and the canonical big-step semantics $\hat{\zeta}$ for the term $(\mathit{II})(\mathit{II})$; the theorem predicts $\hat{\zeta}((\mathit{II})(\mathit{II})) = \hat{\beta}((\mathit{II})(\mathit{II}))$ and that both give the same value only if the rewriting recovers the original multi-step relation, so a mismatch would falsify Theorem 5.4. More generally, a computer search over finite rule sets that satisfy strong separation but yield $\hat{\zeta} \neq \hat{\beta}$ would settle the theorem's scope.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central claim is Theorem 5.4: for every strongly separated abstract HO-GSOS law with an $\omega$-continuous distributive law, the canonical big-step semantics $\hat{\zeta}$ equals the multi-step small-step semantics $\hat{\beta}$ on the computation part. The equality is the abstract form of $t \Downarrow v \iff t \to^{\ast} v \wedge v\downarrow$, and it is established by mutual inequality of least fixed points. The paper also extends the result to languages with variable binders (Theorem 7.3) by reworking the value-forming rules with pointed strength and substitution tensors, obtaining as an instance the call-by-name $\lambda$-calculus. The abstraction isolates, for the first time, a single sufficient condition — strong separation — under which the small-step relation is compatible with evaluation, so the derived big-step rules faithfully execute the strategy that the small-step rules encode.

Load-bearing premise

Strong separation is the load-bearing assumption: without the commutativity condition on rules with computation premises, the derived big-step semantics can diverge from multi-step reduction, as the paper's Example 2.1 shows.

Editorial extensions

If this is right

  • For any language whose small-step rules fit the strongly separated format, the equivalence $t \Downarrow v \iff t \to^{\ast} v \wedge v\downarrow$ is now obtained by theorem rather than by hand; the paper demonstrates this for extended combinatory logic, typed combinatory logic, PCF-style recursion and conditionals, nondeterministic choice, and parallel composition.
  • The translation automatically produces big-step rules from small-step rules; the generated rules have the standard judgement shape $t \Downarrow v$, with values forced to be those terms built from value formers.
  • Call-by-value can be accommodated, but only after rewriting the small-step system with auxiliary composition operators; the resulting big-step semantics matches the original call-by-value multi-step behaviour.
  • The lambda calculus with binders is covered via a presheaf category with a substitution tensor: the abstract equivalence is re-proven in that setting (Theorem 7.3), yielding the usual big-step rules for call-by-name $\lambda$-calculus.
  • Because the equivalence is parametric in syntax and behaviour, the same proof infrastructure applies to other effects captured by $\omega$-continuous monads, with nondeterminism (powerset monad) and partiality as the paper's running examples.

Reading between the lines

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

  • The strong separation condition is effectively a 'no surprises' constraint on rule formats: the paper itself notes its resemblance to cool formats and patience rules; a practical upshot is that language designers who want the equivalence theorem can use it as a checklist and can repair violations by adding auxiliary operators, as done for call-by-value.
  • The parametric proof suggests a testable recipe for new language features: encode the feature as value and computation formers, check strong separation, and the equivalence follows without a bespoke argument; a natural next test is probabilistic or weighted semantics, where a quantitative monad would replace the powerset monad.
  • An implicit consequence is that failures of $\left(\star\right)$ are diagnosable: a separated but not strongly separated specification (such as Example 2.1) provably cannot admit any big-step semantics satisfying the equivalence, so the condition pinpoints why a rule set is too fine-grained for big-step reasoning.
  • The call-by-value treatment suggests a general principle: a big-step semantics over the original signature may not exist, but a definitional extension with auxiliary operators can restore it — connecting the abstract framework to pretty-big-step semantics, as the paper notes.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

2 major / 3 minor

Summary. The paper develops a categorical framework for deriving big-step operational semantics from small-step operational semantics in higher-order mathematical operational semantics. It introduces separated abstract HO-GSOS laws (Definition 3.1), a strong-separation condition (Definition 3.6), and an abstract notion of big-step SOS (Definition 4.1), together with a construction translating a small-step law into a big-step law. The main result, Theorem 5.4, states that for strongly separated abstract HO-GSOS laws with an omega-continuous distributive law, the canonical big-step semantics zeta_hat equals the multi-step small-step semantics beta_hat. The paper presents case studies for typed combinatory logic, recursion and conditionals, nondeterminism and parallelism, call-by-value, and the lambda calculus with binders, and includes Haskell implementations of several examples and proofs in the appendix.

Significance. If the main theorem and its instantiations are fully justified, this is a valuable contribution: it provides a single abstract account of the equivalence between small-step and big-step operational semantics, going beyond syntax-driven translations and covering a wide range of language features. The paper is careful to state hypotheses, gives a counterexample (Example 2.1) showing that strong separation is genuinely needed, and provides detailed appendix proofs for the central lemmas. The Haskell implementation is a useful companion artifact. The main weakness is the gap between the omega-continuity hypothesis of Theorem 5.4 and the deterministic case studies, which are formulated with the identity monad; this gap is repairable but currently affects the scope claims.

major comments (2)
  1. [Section 5, Theorem 5.4; Sections 6.1, 6.2, 6.4] Theorem 5.4 assumes an omega-continuous monad T, as stated at the beginning of Section 5 and needed for the least-fixpoint definitions in (19) and (20). However, the deterministic case studies in Sections 6.1, 6.2, and 6.4 are presented with T = Id, which the paper itself notes is not omega-continuous. Proposition 3.11 is cited as a way to lift a deterministic law to a powerset-valued law, but the paper never proves the required conservative-extension lemma: for every term t, the lifted semantics should satisfy zeta_hat(t) = {v} exactly when t evaluates to v and beta_hat(t) = {v} exactly when t reduces to the value v, and be empty otherwise. Without such a lemma, Theorem 5.4 applies only to the powerset-lifted versions of these examples, not to the deterministic semantics the paper claims to cover.
  2. [Section 6.4, call-by-value] The paragraph claiming that 'for terms in the original signature (without G# and ) we obtain the same big-step semantics as in (25)' and the subsequent claim that the two variants of the small-step semantics are equivalent in multi-step behaviour are stated without proof. This equivalence is load-bearing for the call-by-value case study, because the auxiliary operators G# and are introduced precisely to satisfy strong separation while recovering the original multi-step relation. A proof or at least a precise statement of this example-level equivalence should be provided.
minor comments (3)
  1. [Section 6.4, rule display] The displayed rules for the call-by-value small-step semantics run together in the text; the rules (a), (b), and (c) should be separated clearly, and each rule should be labelled consistently so that the later references to (a1) and (a2) are easy to follow.
  2. [Section 7, Theorem 7.3] The statement of Theorem 7.3 says the proof 'remains essentially unchanged' from that of Theorem 5.4; since the definition of zeta_hat is modified in Section 7.3, it would help the reader to spell out at least the one place where Proposition 7.2 is substituted for Proposition 5.3 and to verify that strong separation still yields the analogue of Lemma 5.1 in the pointed-strength setting.
  3. [Proposition 3.11] The factorization condition in Proposition 3.11 is stated abstractly, and the verification in Remark 3.12 covers only the powerset monad. A brief explanation of how the partiality monad or other omega-continuous monads would satisfy this condition would make the proposition's range of applicability clearer.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: Theorem 5.4 proves the equality of two separately defined least fixpoints; strong separation is an explicit hypothesis, not a renamed version of the conclusion.

full rationale

The central claim is Theorem 5.4, asserting ζ̂ = β̂. These are not the same object by construction: ζ̂ is the least fixpoint (19) of a functional built from the derived big-step transformation ξ (17), while β̂ is the least fixpoint (20) built from the small-step operational model γc. The proof in Section 5 proceeds by mutual inequalities, using Lemmas 5.1 and 5.2, and neither lemma assumes the equality. Strong separation (Definition 3.6) is an explicit structural hypothesis on the small-step law; its role is to make the two approximating chains comparable, and Example 2.1 shows that without it the desired equivalence can fail, so the condition is not a disguised form of the theorem. The big-step rules are derived from the small-step law rather than fitted to the expected answer, and the equality is proved, not postulated. Self-citations to [21] supply the prior abstract HO-GSOS framework and the standard operational model, but the equivalence result and its proof are developed in this paper; Proposition 2.2 is proved in the appendix rather than merely imported. The noted gap concerning ω-continuity of the identity monad and the conservative-extension status of Proposition 3.11 is a scope or verification concern about how the deterministic examples instantiate the theorem, not a circularity in the abstract derivation. Therefore the derivation chain is self-contained and no circular step is exhibited.

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

The central theorem rests on the standard categorical setup (distributive category, free monads, ω-continuous monads), the rule-format axioms of Definition 3.1, the technical complementation assumption, and the paper's new strong separation condition. No numeric parameters are fitted to data; the examples are instances of the framework, not tunings of it.

assumptions (7)
  • standard math The ambient category C is distributive, with finite products and coproducts interacting via the canonical isomorphism.
    Assumed in Section 2.2 and throughout; used for coproduct decompositions such as μΣ ≅ μΣv + μΣc.
  • domain assumption The monad T is strong and ω-continuous, i.e., its Kleisli category is enriched over pointed ω-cpos with continuous strength and copairing.
    Required for the least-fixpoint definitions of β and ζ (equations 19 and 20) and for Kleene's fixpoint theorem; the identity monad is not ω-continuous, which forces lifting via Proposition 3.11 for deterministic examples.
  • domain assumption The separated HO-GSOS law consists of ρv: ΣvX → D(X, Σ*X), ρc: Σc(X×B(X,Y),X) → TΣ*(X+Y), dinatural in X and natural in Y, and a distributive law χ: Σc(TX,Y) → TΣc(X,Y).
    Definition 3.1; this is the rule-format shape inherited and refined from higher-order GSOS [21].
  • standard math Assumption 3.4: the morphisms Σc(inl,id) are complemented, with a natural coproduct decomposition Θ(X,Y,Z) → Σc(X+Y,Z).
    Holds for polynomial signatures by the binomial formula (Remark 3.5); used to split proof obligations in Lemmas 5.1 and 5.2.
  • ad hoc to paper Strong separation condition (Definition 3.6): a commutativity diagram constraining ρc on rules with at least one computation-premise, involving Θ, χ, and copairing.
    Introduced by the authors as a well-behavedness condition on small-step rules; analogous to patience rules in cool GSOS formats and necessary for the equivalence by Example 2.1.
  • domain assumption The distributive law χ is ω-continuous.
    Hypothesis of Theorem 5.4 and of Lemmas 5.1 and 5.2; satisfied by the standard powerset-monad distributive law.
  • domain assumption For the binder extension, C is closed monoidal and the signature Σ'v + ΣcΔ has pointed strength, yielding a monoid structure on the initial algebra μΣ.
    Section 7.1, following Fiore et al.; needed to model substitution and to lift ρv to a form involving jX and jX -• Y.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Big Steps in Higher-Order Mathematical Operational Semantics." pith.science (2026). https://pith.science/paper/ZKI6TTRI

@misc{pith2026250601076,
  author       = {Pith},
  title        = {Pith review of: Big Steps in Higher-Order Mathematical Operational Semantics},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ZKI6TTRI}},
  note         = {Machine review of arXiv:2506.01076}
}
read the original abstract

Small-step and big-step operational semantics are two fundamental styles of structural operational semantics (SOS), extensively used in practice. The former one is more fine-grained and is usually regarded as primitive, as it only defines a one-step reduction relation between a given program and its direct descendant under an ambient evaluation strategy. The latter one implements, in a self-contained manner, such a strategy directly by relating a program to the net result of the evaluation process. The agreement between these two styles of semantics is one of the key pillars in operational reasoning on programs; however, such agreement is typically proven from scratch every time on a case-by-case basis. A general, abstract mathematical argument behind this agreement is up till now missing. We cope with this issue within the framework of higher-order mathematical operational semantics by providing an abstract categorical notion of big-step SOS, complementing the existing notion of abstract higher-order GSOS. Moreover, we introduce a general construction for deriving the former from the latter, and prove an abstract equivalence result between the two.

Figures

Figures reproduced from arXiv: 2506.01076 by the authors.

Figure 1
Figure 1. Operational semantics of call-by-name 𝜆-calculus (small-step and big-step). The main goal of our present work is to provide suitable abstractions for the notions of small￾step and big-step operational semantics, enabling us to formulate and prove (★) at a high level of generality, particularly by parametrizing over suitable notions of syntax and behaviour. To that end, we capitalize on recent advances in higher-orde… view at source ↗
Figure 2
Figure 2. Small-step operational semantics of xCL. transformations. The first-order form of this connection goes back to the seminal work of Turi and Plotkin [37]. Without this leverage, the question of the general connection between small-step and big-step semantics was addressed in the literature in a syntax-driven manner. Ciobâcă [11], motivated similarly to us, proposed an automatic translation of small-step specification… view at source ↗
Figure 3
Figure 3. HOGSOS type class and XCL ′ as its instance. To build intuition for the upcoming technical developments, we present a semi-formal exposition of xCL, including its small-step and big-step operational semantics, as well as their relationship, using Haskell. This exposition serves to motivate and clarify the original notion of higher-order abstract GSOS laws [21] and their separated variant. A rigorous categorical trea… view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: SepHOGSOS type class as a refinement of HOGSOS. that 𝑝 ⇓𝑤 also occurs in the premise. The latter type of rules is thus determined by a choice of an operation from sc, by a choice of an operation from sv for every of its argument that corresponds to the first position o…
Figure 5
Figure 5. Figure 5: BSSOS type class, and SepHOGSOS as its instance. We can now express (★) as the equality beta p t == zeta t (2) for all p :: Proxy d and t :: InitialC sv sc. For a final note, observe that (2), albeit desirable, need not always be true. Example 2.1. Consider a language …
Figure 6
Figure 6. Figure 6: Big-step operational semantics of xCL. also not necessary to restrict to partiality as the only effect – one can treat nondeterministic or even probabilistic semantics in a similar manner. We thus generally work with strong 𝜔-continuous monads, which are arguably the l…

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

41 extracted references · 29 canonical work pages

  1. [1]

    Abramsky

    S. Abramsky. 1990. The lazy 𝜆-calculus. In Research topics in Functional Programming . Addison Wesley, 65–117

    work page 1990

  2. [2]

    Thorsten Altenkirch, Nils Danielsson, and Nicolai Kraus. 2017. Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type. In Foundations of Software Science and Computation Structures, FOSSACS 2017 (LNCS, Vol. 10203), Javier Esparza and Andrzej Murawski (Eds.). 534–549

    work page 2017

  3. [3]

    Guillaume Ambal, Alan Schmitt, and Sergueï Lenglet. 2020. Automatic Transformation of a Big-Step Skeletal Semantics into Small-Step. Ph. D. Dissertation. Inria Rennes-Bretagne Atlantique

    work page 2020

  4. [4]

    Steve Awodey. 2010. Category Theory (2nd ed.). Oxford University Press, Inc., New York, NY, USA

    work page 2010

  5. [5]

    Casper Bach Poulsen and Peter D. Mosses. 2014. Deriving Pretty-Big-Step Semantics from Small-Step Semantics. In Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410 . Springer-Verlag, Berlin, Heidelberg, 270–289. doi:10.1007/978-3-642-54833-8_15

    work page doi:10.1007/978-3-642-54833-8_15 2014

  6. [6]

    Bernstein

    Karen L. Bernstein. 1998. A Congruence Theorem for Structured Operational Semantics of Higher-Order Languages. In 13th Annual IEEE Symposium on Logic in Computer Science, LICS’98 . IEEE Computer Society, 153–164. doi:10.1109/ LICS.1998.705652

    work page arXiv 1998

  7. [7]

    Bard Bloom. 1995. Structural Operational Semantics for Weak Bisimulations. Theor. Comput. Sci. 146, 1&2 (1995), 25–68. doi:10.1016/0304-3975(94)00152-9

    work page doi:10.1016/0304-3975(94)00152-9 1995

  8. [8]

    Venanzio Capretta. 2005. General recursion via coinductive types. Log. Meth. Comput. Sci. 1, 2 (2005)

    work page 2005

Show all 41 references
  1. [9]

    James Chapman, Tarmo Uustalu, and Niccolò Veltri. 2015. Quotienting the Delay Monad by Weak Bisimilarity. In Theoretical Aspects of Computing, ICTAC 2015 (LNCS, Vol. 9399) . Springer, 110–125

    2015

  2. [10]

    Arthur Charguéraud. 2013. Pretty-Big-Step Semantics. In Programming Languages and Systems, Matthias Felleisen and Philippa Gardner (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 41–60

    2013

  3. [11]

    Ştefan Ciobâcă. 2013. From Small-Step Semantics to Big-Step Semantics, Automatically. In Integrated Formal Methods, Einar Broch Johnsen and Luigia Petre (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 347–361

    2013

  4. [12]

    H. B. Curry. 1930. Grundlagen der Kombinatorischen Logik. Am. J. Math. 52, 3 (1930), 509–536. http://www.jstor.org/ stable/2370619

    1930

  5. [13]

    Nils Anders Danielsson. 2012. Operational semantics using the partiality monad. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming (ICFP 2012) . Association for Computing Machinery, New York, NY, USA, 127–138. doi:10.1145/2364527.2364546

    2012

  6. [14]

    Deliguoro and A

    U. Deliguoro and A. Piperno. 1995. Nondeterministic Extensions of Untyped𝜆-Calculus. Information and Computation 122, 2 (1995), 149–177. doi:10.1006/inco.1995.1145

    1995

  7. [15]

    Mariangiola Dezani-Ciancaglini, Ugo de’Liguoro, and Adolfo Piperno. 1998. A Filter Model for Concurrent Lambda- Calculus. SIAM J. Comput. 27, 5 (1998), 1376–1419. doi:10.1137/S0097539794275860

    1998 doi

  8. [16]

    Marcelo P. Fiore. 2008. Second-Order and Dependently-Sorted Abstract Syntax. In 23d Annual IEEE Symposium on Logic in Computer Science (LICS 2008) . IEEE Computer Society, 57–68. doi:10.1109/LICS.2008.38

    2008 doi

  9. [17]

    Fiore, Gordon D

    Marcelo P. Fiore, Gordon D. Plotkin, and Daniele Turi. 1999. Abstract Syntax and Variable Binding. In14th Annual IEEE Symposium on Logic in Computer Science (LICS 1999) . IEEE Computer Society, 193–202. doi:10.1109/LICS.1999.782615

    1999

  10. [18]

    Gallagher, Manuel Hermenegildo, Bishoksan Kafle, Maximiliano Klemen, Pedro López García, and José Morales

    John P. Gallagher, Manuel Hermenegildo, Bishoksan Kafle, Maximiliano Klemen, Pedro López García, and José Morales

  11. [19]

    Sergey Goncharov. 2021. Uniform Elgot Iteration in Foundations. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021) (LIPIcs, Vol. 198) , Nikhil Bansal, Emanuela Merelli, and James Worrell (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informat...

    2021

  12. [20]

    Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. 2022. Stateful Structural Operational Semantics. In 7th International Conference on Formal Structures for Computation and Deduction, FSCD’22 (LIPIcs, Vol. 228), Amy P. Felty (Ed.). Schloss Dags...

    2022 doi

  13. [21]

    Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. 2023. Towards a Higher-Order Mathematical Operational Semantics. Proc. ACM Program. Lang. 7, POPL (2023), 632–658. doi:10.1145/3571215

    2023 doi

  14. [22]

    Sergey Goncharov, Alessio Santamaria, Lutz Schröder, Stelios Tsampas, and Henning Urbat. 2024. Logical Predicates in Higher-Order Mathematical Operational Semantics. In Foundations of Software Science and Computation Structures , Naoki Kobayashi and James Worrell (Eds.). Sprin...

    2024

  15. [23]

    Sergey Goncharov, Lutz Schröder, Christoph Rauch, and Julian Jakob. 2018. Unguarded Recursion on Coinductive Resumptions. Log. Methods Comput. Sci. 14, 3 (2018)

    2018

  16. [24]

    Andrew D. Gordon. 1999. Bisimilarity as a Theory of Functional Programming. Theor. Comput. Sci. 228, 1-2 (1999), 5–47. doi:10.1016/S0304-3975(98)00353-3

    1999 doi

  17. [25]

    Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. 2007. Generic Trace Semantics via Coinduction. Logical Methods in Computer Science 3, 4 (2007). doi:10.2168/LMCS-3(4:11)2007 28 Sergey Goncharov, Pouya Partow, and Stelios Tsampas

    2007 doi

  18. [26]

    Roger Hindley and Jonathan P

    J. Roger Hindley and Jonathan P. Seldin. 2008. Lambda-Calculus and Combinators: An Introduction (2 ed.). Cambridge University Press. doi:10.1017/CBO9780511809835

    2008 doi

  19. [27]

    André Hirschowitz, Tom Hirschowitz, Ambroise Lafont, and Marco Maggesi. 2022. Variable binding and substitution for (nameless) dummies. In 25th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2022) (LNCS, Vol. 13242). Springer, 3...

    2022 doi

  20. [28]

    Anders Kock. 1972. Strong Functors and Monoidal Monads. Archiv der Mathematik 23, 1 (1972), 113–120

    1972

  21. [29]

    Ugo Dal Lago and Margherita Zorzi. 2012. Probabilistic operational semantics for the lambda calculus. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 46, 3 (2012), 413–450. doi:10.1051/ita/ 2012012

    2012 doi

  22. [30]

    James Laird. 2016. Weighted Relational Models for Mobility. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 52) , Delia Kesner and Brigitte Pientka (Eds.). Schloss D...

    2016 doi

  23. [31]

    Mac Lane

    S. Mac Lane. 1978. Categories for the Working Mathematician (2 ed.). Graduate Texts in Mathematics, Vol. 5. Springer. http://link.springer.com/10.1007/978-1-4757-4721-8

    1978 doi

  24. [32]

    John McCarthy. 1959. A Basis for a Mathematical Theory of Computation. In Computer Programming and Formal Systems, P. Braffort and D. Hirschberg (Eds.). Studies in Logic and the Foundations of Mathematics, Vol. 26. Elsevier, 33–70. doi:10.1016/S0049-237X(09)70099-0

    1959 doi

  25. [33]

    Mitchell

    John C. Mitchell. 1996. Foundations for programming languages . MIT Press

    1996

  26. [34]

    Eugenio Moggi. 1991. Notions of Computation and Monads. Inf. Comput. 93, 1 (1991), 55–92. doi:10.1016/0890- 5401(91)90052-4

    1991 doi

  27. [35]

    Myreen, Ramana Kumar, and Yong Kiam Tan

    Scott Owens, Magnus O. Myreen, Ramana Kumar, and Yong Kiam Tan. 2016. Functional Big-Step Semantics. In Proceedings of the 25th European Symposium on Programming Languages and Systems - Volume 9632 . Springer-Verlag, Berlin, Heidelberg, 589–615. doi:10.1007/978-3-662-49498-1_23

    2016 doi

  28. [36]

    Stelios Tsampas, Christian Williams, Andreas Nuyts, Dominique Devriese, and Frank Piessens. 2021. Abstract Congruence Criteria for Weak Bisimilarity. In 46th International Symposium on Mathematical Foundations of Computer Science, MFCS’21 (LIPIcs, Vol. 202), Filippo Bonchi and...

    2021 doi

  29. [37]

    Daniele Turi and Gordon D. Plotkin. 1997. Towards a Mathematical Operational Semantics. In 12th Annual IEEE Symposium on Logic in Computer Science (LICS 1997) . 280–291. doi:10.1109/LICS.1997.614955

    1997

  30. [38]

    Henning Urbat, Stelios Tsampas, Sergey Goncharov, Stefan Milius, and Lutz Schröder. 2023. Weak Similarity in Higher-Order Mathematical Operational Semantics. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 1–13. doi:10.1109/LICS56636.2023.10175706

    2023

  31. [39]

    Tarmo Uustalu. 2013. Coinductive big-step semantics for concurrency. Electronic Proceedings in Theoretical Computer Science, EPTCS 137 (2013), 63–78

    2013

  32. [40]

    van Glabbeek

    Rob J. van Glabbeek. 2011. On cool congruence formats for weak bisimulations. Theor. Comput. Sci. 412, 28 (2011), 3283–3302. doi:10.1016/j.tcs.2011.02.036 Big Steps in Higher-Order Mathematical Operational Semantics 29 A OMITTED PROOFS A.1 Proof of Proposition 2.2 We have the ...

    2011 doi

  33. [2020]

    In Electronic Proceedings in Theoretical Computer Science, EPTCS , Vol

    From big-step to small-step semantics and back with interpreter specialisation. In Electronic Proceedings in Theoretical Computer Science, EPTCS , Vol. 320. Open Publishing Association, 50–64. doi:10.4204/EPTCS.320.4

    doi

Pith tools

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