A Word Sampler for Well-Typed Functions
Breandan Considine

TL;DR
This paper introduces an exact, uniform sampler for well-typed functions in a simply-typed language, leveraging automata and grammars to ensure type soundness and completeness.
Contribution
It presents a novel reduction from a syntax-directed type system to a context-free grammar that preserves type properties and enables efficient sampling.
Findings
Samples uniformly from well-typed functions
Maintains type soundness and completeness
Uses fixed-parameter tractable reduction
Abstract
We describe an exact sampler for a simply-typed, first-order functional programming language. Given an acyclic finite automaton, , it samples a random function uniformly without replacement from well-typed functions in . This is achieved via a fixed-parameter tractable reduction from a syntax-directed type system to a context-free grammar, preserving type soundness and completeness w.r.t. , while retaining the robust metatheory of formal languages.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · semigroups and automata theory · Formal Methods in Verification
