pith. sign in

arxiv: 2606.22616 · v1 · pith:AEK2KBITnew · submitted 2026-06-21 · 💻 cs.PL

Compositional Generator Equivalence (Extended Version)

Anthony Vandikas , Kiarash Sotoudeh , Marsha Chechik This is my paper

Pith reviewed 2026-06-26 09:19 UTC · model grok-4.3

classification 💻 cs.PL
keywords property-based testingcompositional semanticsgenerator equivalenceHedgehogarrow calculusdistribution semanticssampling semanticsprogram optimization
0
0 comments X

The pith

Any sound and complete compositional semantics for Hedgehog must match its sampling semantics, which blocks common optimizations, but a restricted arrow-calculus version admits a compositional distribution semantics.

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

The paper shows that Hedgehog's distribution semantics, meant to capture how users reason about generators for property-based testing, fails to be compositional. It proves that any alternative compositional semantics that is both sound and complete with respect to the original language must collapse to the sampling semantics, which tracks every possible execution path and is too fine-grained to justify typical generator rewrites. To escape this impasse the authors define Hedgehog→, a fragment built on the arrow calculus, and prove that it possesses a compositional distribution semantics. A Haskell implementation demonstrates that the restriction still captures generators used in practice.

Core claim

Hedgehog's distribution semantics is non-compositional; any sound and complete compositional semantics for the full language is necessarily equivalent to its sampling semantics; and the arrow-calculus restriction Hedgehog→ possesses a compositional distribution semantics while remaining expressive enough for generators of practical interest.

What carries the argument

Hedgehog→, the arrow-calculus restriction whose distribution semantics is compositional and therefore supports equivalence proofs between generators.

If this is right

  • Common generator rewrites cannot be justified by compositional reasoning inside the original Hedgehog language.
  • Equivalence proofs between generators become possible inside Hedgehog→ because its distribution semantics is compositional.
  • The sampling semantics remains available for implementation while the distribution semantics can be used for high-level reasoning in the restricted language.
  • Optimizations that preserve the distribution semantics can now be validated compositionally for the class of generators expressible in Hedgehog→.

Where Pith is reading between the lines

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

  • The same tension between compositionality and granularity may appear in other property-based testing frameworks that expose similar generator combinators.
  • Tooling that automatically rewrites generators could be built on top of the compositional distribution semantics once the restriction is adopted.
  • Users may still write full Hedgehog generators and then mechanically translate the parts that need equivalence proofs into the arrow fragment.

Load-bearing premise

The distribution semantics correctly models how users reason about generators and the arrow-calculus restriction is still expressive enough to write generators of practical interest.

What would settle it

A counter-example generator that is expressible in Hedgehog→ yet cannot be given a compositional distribution semantics, or a concrete optimization whose correctness cannot be proved even inside Hedgehog→.

Figures

Figures reproduced from arXiv: 2606.22616 by Anthony Vandikas, Kiarash Sotoudeh, Marsha Chechik.

Figure 1
Figure 1. Figure 1: Example generators and distinguishing context. The generator [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Trees produced by discrim (see [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Miscellaneous Functions FB = B FN = N FR≥0 = Borel { (𝑟, 𝑟′ ) | 𝑟 < 𝑟 ′ ∈ R≥0 } FS = Borel { (𝑟, 𝑟′ ) | 𝑟 < 𝑟 ′ ∈ S } [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 5
Figure 5. Figure 5: Common Sets of Random Variables. 𝑓 ◦ arrid = 𝑓 (𝑓 ◦ 𝑔) ◦ ℎ = 𝑓 ◦ (𝑔 ◦ ℎ) arr (𝑓 ◦ 𝑔) = arr 𝑓 ◦ arr𝑔 first (arr 𝑓 ) = arr (𝑓 × id) first (𝑓 ◦ 𝑔) = first 𝑓 ◦ first𝑔 arr (id × 𝑔) ◦ first 𝑓 = first 𝑓 ◦ arr (id × 𝑔) arr (−1) ◦ first 𝑓 = 𝑓 ◦ arr (−1) arr assoc ◦ first (first 𝑓 ) = first 𝑓 ◦ arr assoc [PITH_FULL_IMAGE:figures/full_fig_p006_5.png] view at source ↗
Figure 7
Figure 7. Figure 7: Integral Properties. Monad Operations unit : 𝐴 →Q List𝐴 unit 𝑎 = 𝑎 :: 𝜖 bind : (𝐴 →Q List 𝐵) →Q List𝐴 →Q List 𝐵 bind 𝑓 𝜖 = 𝜖 bind 𝑓 (𝑎 :: 𝑎𝑠) = 𝑓 𝑎 ++ bind 𝑓 𝑎𝑠 unit : 𝐴 →Q Tree𝐴 unit 𝑎 = node (𝑎, 𝜖) bind : (𝐴 →Q Tree 𝐵) →Q Tree𝐴 →Q Tree 𝐵 bind 𝑓 (node (𝑎, 𝑎𝑠)) = node (𝑏, 𝑏𝑠 ++ map (bind 𝑓 ) 𝑎𝑠) where node (𝑏, 𝑏𝑠) = 𝑓 𝑎 Auxiliary Definitions (++) : List𝐴 × List𝐴 →Q List𝐴 𝜖 ++ 𝑏𝑠 = 𝑏𝑠 (𝑎 :: 𝑎𝑠) ++ 𝑏𝑠 = 𝑎 ::… view at source ↗
Figure 8
Figure 8. Figure 8: Lists and Rose Trees. the distributions map 𝑓 𝜇 ∈ Dist 𝐵 (called the push-forward of 𝑓 on 𝜇) and 𝑐 · 𝜇 ∈ Dist𝐴 satisfy the properties ∫ 𝑔 d(map 𝑓 𝜇) = ∫ 𝑔 ◦ 𝑓 d𝜇 ∫ ℎ d(𝑐 · 𝜇) = 𝑐 · ∫ ℎ d𝜇 for all 𝑔 : 𝐵 →Q R≥0 and ℎ : 𝐴 →Q R≥0. The uniform distribution on samples 𝜆 ∈ Dist S is the (unique) distribution satisfying ∫ 𝜎 [𝜎1 ≤ 𝜎 ≤ 𝜎2] d𝜆 = 𝜎2 − 𝜎1 for all 𝜎1 ≤ 𝜎2 ∈ S. There exists two functions 𝜋𝑙 , 𝜋𝑟 : S → S … view at source ↗
Figure 9
Figure 9. Figure 9: Derived Constructs. Γ, 𝑥 : 𝜏 ⊢ 𝑥 : 𝜏 Γ ⊢ 𝑡 : 𝜏1 Γ ⊢ inl 𝑡 : 𝜏1 + 𝜏2 Γ ⊢ 𝑡 : 𝜏2 Γ ⊢ inr 𝑡 : 𝜏1 + 𝜏2 Γ ⊢ 𝑡 : 0 Γ ⊢ absurd 𝑡 : 𝜏 𝑥1, 𝑥2 ∉ Dom Γ Γ ⊢ 𝑡0 : 𝜏1 + 𝜏2 Γ, 𝑥1 : 𝜏1 ⊢ 𝑡1 : 𝜏3 Γ, 𝑥2 : 𝜏2 ⊢ 𝑡2 : 𝜏3 Γ ⊢ match 𝑡0 with inl 𝑥1. 𝑡1 | inr 𝑥2. 𝑡2 : 𝜏3 Γ ⊢ () : 1 Γ ⊢ 𝑡1 : 𝜏1 Γ ⊢ 𝑡2 : 𝜏2 Γ ⊢ (𝑡1, 𝑡2) : 𝜏1 * 𝜏2 Γ ⊢ 𝑡 : 𝜏1 * 𝜏2 Γ ⊢ fst 𝑡 : 𝜏1 Γ ⊢ 𝑡 : 𝜏1 * 𝜏2 Γ ⊢ snd 𝑡 : 𝜏2 𝑥 ∉ Dom Γ Γ, 𝑥 : 𝜏1 ⊢ 𝑡 : 𝜏2 Γ ⊢ fun 𝑥 : 𝜏… view at source ↗
Figure 10
Figure 10. Figure 10: Hedgehog’s Typing Rules. Example 3.2. We recast our examples from Section 1 in our chosen syntax, modelling bool_ as flip 1/2: coin1 = let 𝑥 ← flip 1/2 in let 𝑦 ← flip 1/2 in return 𝑥 = 𝑦 coin2 = let 𝑥 ← flip 1/2 in return 𝑥 Definition 3.3 (Hedgehog Environments and Typing). An environment Γ ∈ Î 𝑥 ∈Dom Γ Type is a family mapping variables from a finite domain Dom Γ ⊆ Var to types. The set of environments … view at source ↗
Figure 11
Figure 11. Figure 11: Semantics of Hedgehog. An interpretation induces (1) a type and environment semantics ⟦−⟧ 𝐹 : Type ∪ Env → Qbs and (2) for all Γ ⊢ 𝑡 : 𝜏 a term semantics ⟦Γ ⊢ 𝑡 : 𝜏⟧ 𝐹 : ⟦Γ⟧ 𝐹 →Q ⟦𝜏⟧ 𝐹 (see [PITH_FULL_IMAGE:figures/full_fig_p010_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Hedgehog’s Sampling Interpretation. Definition 3.4 is that it is compositional, i.e., the semantics of a term is uniquely determined by the semantics of its immediate sub-terms. Definition 3.5 (Hedgehog Sampling Interpretation). The sampling interpretation ℭ : Qbs → Qbs of Hedgehog is defined in [PITH_FULL_IMAGE:figures/full_fig_p011_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Hedgehog→ Command Semantics. We similarly wrap the function discrim as discrim• : (1 ⇝ Bool)  (1 ⇝ Bool) discrim• = fun 𝑓 : 1 ⇝ Bool. fun 𝑢 : 1. let 𝑏 ← shrink (true, false) in if 𝑏 then 𝑓 () else coin• 1 (). 4.2 Semantics Definition 4.4 (Hedgehog→ Interpretation and Semantics). A Hedgehog→ interpretation 𝐹 : Qbs × Qbs → Qbs is a pre-arrow equipped with additional operations flip𝐹 : [0, 1] →Q 𝐹 (1, B) sh… view at source ↗
Figure 14
Figure 14. Figure 14: Hedgehog→’s Sampling Interpretation. command terms. One significant difference is that the semantics of match (specifically within a command term) is now also defined by the interpretation. As with Definition 3.4, we only require an interpretation to be a pre-arrow and not an arrow, since our sampling interpretation is not an arrow. Definition 4.5 (Hedgehog→ Sampling Interpretation). The sampling interpre… view at source ↗
Figure 15
Figure 15. Figure 15: Hedgehog→’s Distribution Interpretation. Like Hedgehog, Hedgehog→ interpretations induce a semantic equivalence relation. Definition 4.8 (Hedgehog→ Semantic Equivalence). Two Hedgehog→ terms Γ ⊢ • 𝑡1, 𝑡2 : 𝜏 are seman￾tically equivalent with respect to an interpretation 𝐹 (written Γ ⊢ • 𝑡1 = 𝐹 𝑡2 : 𝜏) if ⟦Γ ⊢ • 𝑡1 : 𝜏⟧ 𝐹 = ⟦Γ ⊢ • 𝑡2 : 𝜏⟧ 𝐹 . We write 𝑡1 = 𝐹 𝑡2 : 𝜏 for () ⊢ • 𝑡1 = 𝐹 𝑡2 : 𝜏 and omit the typ… view at source ↗
Figure 16
Figure 16. Figure 16: Translation from Hedgehog→ to Hedgehog. Proposition 4.16. The following equivalence holds: let 𝑥 ← flip 𝑝 in if 𝑥 then 𝑡 else 𝑡 = 𝔇 𝑡 (11′ ) Intuitively, Proposition 4.16 demonstrates that equation (11) holds whenever the condition term does not shrink. 4.4 From Hedgehog→ to Hedgehog Definition 4.17. The translation from Hedgehog→ types, environments, and terms to Hedgehog types, environments, and terms i… view at source ↗
Figure 17
Figure 17. Figure 17: Example 4.3 translated to Haskell. (match) to produce statistically independent values. This cannot be a simple semantic change due to the presence of higher-order computation, so Hedgehog→ also places restrictions on (effectful) function application in the style of the arrow calculus [Lindley et al. 2010]. The resulting language admits nearly all the program transformations discussed in Theorems 3.8 and … view at source ↗
Figure 18
Figure 18. Figure 18: The prune Function. Module # Expressible Module Size Hedgehog.Gen 2/4/70 (76) N/A Test.Example.Basic 0/5/13 (18) 417/393 (6.1%) Test.Example.Confidence 0/0/1 (1) 35/37 (-5.4%) Test.Example.Coverage 0/0/7 (7) 251/261 (-3.8%) Test.Example.Exception 0/0/3 (3) 82/85 (-3.5%) Test.Example.QuasiShow 0/0/2 (2) 63/60 (5%) Test.Example.Resource 0/0/3 (3) 398/401 (-0.7%) Test.Example.RoundTrip 0/3/0 (6) 225/216 (4.2… view at source ↗
Figure 19
Figure 19. Figure 19: The implementation of choice in Hedgehog. RQ2: What is the impact of Hedgehog→’s design on program size? The restrictions Hedgehog→ places on command terms may require users to employ verbose workarounds. We determine whether this is the case by measuring the impact of Hedgehog→’s design on program size [PITH_FULL_IMAGE:figures/full_fig_p027_19.png] view at source ↗
read the original abstract

Property-based testing (PBT) is a powerful technique for software verification that relies on random input generators and "shrinking" processes to find and minimize counterexamples to executable specifications called properties. While optimizing these generators is crucial for testing efficiency, formally justifying such optimizations is currently difficult because existing languages lack a compositional semantics that is coarse-grained enough for high-level reasoning. In this paper, we first provide a formal account of the syntax and semantics of Hedgehog, a popular PBT framework. We demonstrate that Hedgehog's distribution semantics - which models how users typically reason about generators - is non-compositional. Furthermore, we prove that any sound and complete compositional semantics for Hedgehog must necessarily be equivalent to its sampling semantics, which is too fine-grained to justify common program optimizations. To resolve this dilemma, we introduce Hedgehog$^\rightarrow$, a restricted version of the language based on the arrow calculus, and prove that Hedgehog$^\rightarrow$ possesses a compositional distribution semantics. We evaluate Hedgehog$^\rightarrow$ through a Haskell implementation and show that it remains expressive enough to capture generators of practical interest, while providing the formal foundation needed for compositional generator equivalence proofs.

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

0 major / 3 minor

Summary. The paper provides a formal account of the syntax and semantics of Hedgehog, a property-based testing framework. It proves that Hedgehog's distribution semantics is non-compositional, that any sound and complete compositional semantics must coincide with the sampling semantics (which is too fine-grained for justifying optimizations), and that the restricted Hedgehog→ language (based on the arrow calculus) admits a compositional distribution semantics. It backs this with a Haskell implementation claimed to retain practical expressiveness for generators of interest.

Significance. If the central claims hold, the work supplies a formal foundation for compositional reasoning about generator equivalence in PBT, directly addressing the difficulty of justifying optimizations. The non-compositionality result and the arrow-calculus restriction are technically substantive; the implementation evaluation provides evidence that the restriction does not eliminate practical use cases. Machine-checked proofs or fully reproducible artifacts would further strengthen the contribution.

minor comments (3)
  1. §3 (or wherever the non-compositionality proof appears): clarify whether the counterexample relies on specific features of the distribution semantics definition or holds more generally for any probabilistic semantics with the given monadic structure.
  2. The Haskell implementation section: include a brief comparison table of expressiveness (e.g., number of generators from the original Hedgehog suite that can be directly ported) to make the practicality claim easier to assess.
  3. Notation for the arrow calculus embedding: ensure that the translation from Hedgehog→ programs to arrows is defined equationally in one place so readers can verify preservation of the distribution semantics.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the paper and for recommending minor revision. The report does not list any specific major comments under the MAJOR COMMENTS section.

Circularity Check

0 steps flagged

No circularity: formal proofs rest on independent definitions and theorems

full rationale

The paper defines syntax, sampling semantics, and distribution semantics for Hedgehog from first principles, then proves non-compositionality and the forced equivalence of any sound/complete compositional semantics to the sampling semantics via explicit theorems. Hedgehog→ is introduced as an arrow-calculus restriction with its own compositional semantics proved separately. No step reduces a claimed result to a fitted parameter, self-definition, or load-bearing self-citation; all derivations are self-contained against the stated formal model and external Haskell implementation.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on standard mathematical definitions of semantics and the arrow calculus; no free parameters or new entities are introduced beyond the language restriction.

axioms (1)
  • standard math Standard properties of the arrow calculus for composing computations
    The paper bases Hedgehog→ on the arrow calculus, assuming its known compositional properties.

pith-pipeline@v0.9.1-grok · 5736 in / 1154 out tokens · 31366 ms · 2026-06-26T09:19:12.469121+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

29 extracted references · 17 canonical work pages

  1. [1]

    1995.Domain theory

    Samson Abramsky and Achim Jung. 1995.Domain theory. Oxford University Press, Inc., USA, 1–168. Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. 2006.Compilers: Principles, Techniques, and Tools (2nd Edition). Addison-Wesley Longman Publishing Co., Inc., USA. Emanuele Bandini and Roberto Segala

    1995

  2. [2]

    InFM 2009: Formal Methods, Ana Cavalcanti and Dennis R

    Unifying Probability with Nondeterminism. InFM 2009: Formal Methods, Ana Cavalcanti and Dennis R. Dams (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 467–482. Koen Claessen and John Hughes

    2009

  3. [3]

    QuickCheck: a lightweight tool for random testing of Haskell programs. InProceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00), Montreal, Canada, September 18-21, 2000, Martin Odersky and Philip Wadler (Eds.). ACM, New York, NY, 268–279. doi:10.1145/351240.351266 Koen Claessen, Michal Palka, Nicholas Smallbone,...

    work page doi:10.1145/351240.351266 2000

  4. [4]

    2009), 149–160

    Finding race conditions in Erlang with QuickCheck and PULSE.SIGPLAN Not.44, 9 (Aug. 2009), 149–160. doi:10.1145/1631687. 1596574 Ryan Culpepper and Andrew Cobb

    work page doi:10.1145/1631687 2009

  5. [5]

    Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring. InProgramming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings(Uppsala, Sweden). Springer-Ver...

    work page doi:10.1007/978-3-662-54434-1_14 2017

  6. [6]

    Decomposing Probabilistic Lambda-Calculi. InFoundations of Software Science and Computation Structures: 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings(Dublin, Ireland). Springer-Verlag, Berlin, Heidelberg, 136–156. d...

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

  7. [7]

    InProceedings of the 16th ACM SIGPLAN International Haskell Symposium, Haskell 2023, Seattle, W A, USA, September 8-9, 2023, Trevor L

    falsify: Internal Shrinking Reimagined for Haskell. InProceedings of the 16th ACM SIGPLAN International Haskell Symposium, Haskell 2023, Seattle, W A, USA, September 8-9, 2023, Trevor L. McDonell and Niki Vazou (Eds.). ACM, , Vol. 1, No. 1, Article . Publication date: June

    2023

  8. [8]

    doi:10.1145/3609026.3609733 Emil Eriksson

    30 Anthony Vandikas, Kiarash Sotoudeh, and Marsha Chechik New York, NY, 97–109. doi:10.1145/3609026.3609733 Emil Eriksson

    work page doi:10.1145/3609026.3609733

  9. [9]

    In2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

    Lambda Calculus and Probabilistic Computation. In2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 1–13. doi:10.1109/LICS.2019.8785699 Andrew Farmer, Andy Gill, Ed Komp, and Neil Sculthorpe

    work page doi:10.1109/lics.2019.8785699 2019

  10. [10]

    InProceedings of the 2012 Haskell Symposium(Copenhagen, Denmark) (Haskell ’12)

    The HERMIT in the machine: a plugin for the interactive transformation of GHC core language programs. InProceedings of the 2012 Haskell Symposium(Copenhagen, Denmark) (Haskell ’12). Association for Computing Machinery, New York, NY, USA, 1–12. doi:10.1145/2364506.2364508 Jeremy Gibbons and Ralf Hinze

    work page doi:10.1145/2364506.2364508 2012

  11. [11]

    2011), 2–14

    Just do it: simple monadic equational reasoning.SIGPLAN Not.46, 9 (Sept. 2011), 2–14. doi:10.1145/2034574.2034777 Harrison Goldstein, Samantha Frohlich, Meng Wang, and Benjamin C Pierce

    work page doi:10.1145/2034574.2034777 2011

  12. [12]

    Proceedings of the ACM on Programming Languages7, ICFP (2023), 322–355

    Reflecting on Random Generation. Proceedings of the ACM on Programming Languages7, ICFP (2023), 322–355. Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang

    2023

  13. [13]

    Generalising monads to arrows.Sci. Comput. Program.37, 1–3 (May 2000), 67–111. doi:10.1016/S0167- 6423(99)00023-4 John Hughes

    work page doi:10.1016/s0167- 2000

  14. [14]

    InProceedings of the 5th International Conference on Advanced Functional Programming(Tartu, Estonia)(AFP’04)

    Programming with arrows. InProceedings of the 5th International Conference on Advanced Functional Programming(Tartu, Estonia)(AFP’04). Springer-Verlag, Berlin, Heidelberg, 73–129. doi:10.1007/11546382_2 Robert Krook, Nicholas Smallbone, Bo Joel Svensson, and Koen Claessen

    work page doi:10.1007/11546382_2

  15. [15]

    Sam Lindley, Philip Wadler, and Jeremy Yallop

    QuickerCheck: Implementing and Evaluating a Parallel Run-Time for QuickCheck(IFL 2023). Sam Lindley, Philip Wadler, and Jeremy Yallop

    2023

  16. [16]

    The arrow calculus.J. Funct. Program.20, 1 (2010), 51–69. doi:10.1017/ S095679680999027X Jason Lyngle

    2010

  17. [17]

    Open Source Softw

    Hypothesis: A new approach to property-based testing.J. Open Source Softw. 4, 43 (2019),

    2019

  18. [18]

    doi:10.21105/JOSS.01891 Conor Mcbride and Ross Paterson

    work page doi:10.21105/joss.01891

  19. [19]

    Applicative programming with effects.J. Funct. Program.18, 1 (Jan. 2008), 1–13. doi:10.1017/S0956796807006326 Michael Mislove, Joël Ouaknine, and James Worrell

    work page doi:10.1017/s0956796807006326 2008

  20. [20]

    Eugenio Moggi

    Axioms for probability and nondeterminism.Electronic Notes in Theoretical Computer Science96 (2004), 7–28. Eugenio Moggi

    2004

  21. [21]

    Comput.93, 1 (1991), 55–92

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

    work page doi:10.1016/0890-5401(91)90052- 1991

  22. [22]

    2001), 229–240

    A new notation for arrows.SIGPLAN Not.36, 10 (Oct. 2001), 229–240. doi:10.1145/507669.507664 Gordon D. Plotkin

    work page doi:10.1145/507669.507664 2001

  23. [23]

    LCF Considered as a Programming Language.Theor. Comput. Sci.5, 3 (1977), 223–255. doi:10.1016/ 0304-3975(77)90044-5 Jaro Reinders

    1977

  24. [24]

    InProceedings of the 17th ACM SIGPLAN International Haskell Symposium(Milan, Italy)(Haskell 2024)

    Higher Order Patterns for Rewrite Rules. InProceedings of the 17th ACM SIGPLAN International Haskell Symposium(Milan, Italy)(Haskell 2024). Association for Computing Machinery, New York, NY, USA, 14–26. doi:10.1145/3677999.3678275 Cynthia Richey, Joseph W. Cutler, Harrison Goldstein, and Benjamin C. Pierce

    work page doi:10.1145/3677999.3678275 2024

  25. [25]

    Jacob Stanley

    Fail Faster: Staging and Fast Randomness for High-Performance PBT.Proceedings of the ACM on Programming Languages(2026). Jacob Stanley

    2026

  26. [26]

    Commutative Semantics for Probabilistic Programming. InProgramming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings(Uppsala, Sweden). Springer-Verlag, Berlin, Heidelberg, 855–879. doi:10.10...

    work page doi:10.1007/978-3-662-54434-1_32 2017

  27. [27]

    frasertweedale.github.io/blog-fp/posts/2020- 03-31-quickcheck-hedgehog.html#shrinking-performance Matthijs Vákár, Ohad Kammar, and Sam Staton

    Migrating from QuickCheck to Hedgehog: mixed results. frasertweedale.github.io/blog-fp/posts/2020- 03-31-quickcheck-hedgehog.html#shrinking-performance Matthijs Vákár, Ohad Kammar, and Sam Staton

    2020

  28. [28]

    [VMA19] Andrea Vezzosi, Anders M¨ ortberg, and Andreas Abel

    A domain theory for statistical probabilistic programming.Proc. ACM Program. Lang.3, POPL, Article 36 (Jan. 2019), 29 pages. doi:10.1145/3290349 Daniele Varacca and Glynn Winskel

    work page doi:10.1145/3290349 2019

  29. [29]

    Distributing probability over non-determinism.Mathematical structures in computer science16, 1 (2006), 87–113. , Vol. 1, No. 1, Article . Publication date: June 2026

    2006