Hedgehog distribution semantics is non-compositional; any compositional semantics equals sampling semantics; Hedgehog→ provides compositional semantics via arrow calculus while remaining expressive.
QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs,
11 Pith papers cite this work. Polarity classification is still indexing.
11
Pith papers citing it
citation-role summary
background 3
citation-polarity summary
roles
background 3polarities
background 3representative citing papers
Introduces a Datalog framework modeling CRDT semantics as logic programs for automated analysis, property-based testing, and evaluation on a collaborative graph editing case study.
Underapproximate types with symbolic traces guide synthesis of test generators that outperform defaults in property-based testing and model checking for effectful programs.
A Lean library called Palamedes uses synthesis rules from generator semantics and catamorphism-anamorphism rewriting to automatically produce correct constrained random generators.
ContractEval benchmark on 364 tasks shows code LLMs achieve 75-82% functional pass@1 but 0% contract satisfaction under standard prompting, rising only to 23-41% with explicit contracts.
A symbolic protocol operationalizes Peirce's tripartite reasoning for LLMs using five algebraic invariants including a Weakest Link bound to enforce logical consistency and prevent weak premises from supporting strong conclusions.
Aporia makes design decisions explicit and interactive in AI-assisted programming, leading to higher engagement and 5x fewer mental model disagreements with code in a 14-person user study compared to a baseline agent.
CopilotVerifier generates bisimulation proofs via Crucible symbolic execution and What4 SMT to establish output equivalence and identical crash behavior between Copilot monitors and their compiled forms.
GraphFlow is an architecture for formally verifiable visual workflows that treats diagrams as executable specs with proof-checkable contracts, backed by a pilot of 8728 runs at 97.08% completion on an early prototype without the verified core.
citing papers explorer
-
Trace-Guided Synthesis of Effectful Test Generators
Underapproximate types with symbolic traces guide synthesis of test generators that outperform defaults in property-based testing and model checking for effectful programs.