Type-Directed Program Synthesis for APIs
Casting API discovery as proof search — synthesizing well-typed programs from type signatures.
Composing functions across large libraries and web APIs is hard. I synthesize such code from type signatures by casting it as proof search, using type-guided abstraction refinement to search soundly and efficiently across Haskell libraries (Hoogle+) and RESTful APIs. Ongoing work extends type-directed synthesis to scientific workflow synthesis, integration with LLMs, and automated proof generation for software verification.