Synthesizing Runners Using Copatterns
summary
Deductive synthesis produces an adapter (runner) from coinductive copatterns specifications that filters environment behaviors into client-expected traces; the procedure reduces simulation obligations and emits OCaml shallow handlers. Implementation called appear accepts copattern definitions, runs in ~10–150s on benchmarks, and yields schedulers within 12–15% of Picos performance. The adapter only removes mismatches (no new behaviors), handles cancellation and scheduling patterns, and compiles to runnable OCaml handlers.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:46Effect signatures and runners
- 4:34Adapters for behavior matching
- 6:42Synthesis problem with specs
- 9:51Copatterns for behavior spec
- 11:56Synthesized adapter example
- 13:41Synthesis procedure overview
- 15:50Synthesis rule for mismatch
- 17:37Soundness of synthesis
- 18:59Copatterns to shallow handlers
- 20:24Tool implementation and eval
- 22:27Conclusion
- 23:38Q&A
related talks
14mRelational Synthesis for Pattern Matching
32mHole Refinements for Polymorphic Type-and-Example Driven Synthesis
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
39mDependent Type Driven Program Synthesis in Idris
29mPredicate Dispatch
31mLetting users do the undecidable: lessons from program synthesis
15mMetaprogramming with Combinators
25mRecursive Program Synthesis using Paramorphisms