Augmenting Type Signatures for Program Synthesis
Effective program synthesis requires a way to minimise the number of candidate programs being searched. A type signature, for example, places some small restrictions on the structure of potential candidates. We introduce and motivate a distilled program synthesis problem where a type signature is the only machine-readable information available, but does not sufficiently minimise the search space. To address this, we develop a system of property relations that can be used to flexibly encode and query information that was not previously available to the synthesiser. Our experience using these tools has been positive: by encoding simple properties and by using a minimal set of synthesis primitives, we have been able to synthesise complex programs in novel contexts.
Sun 18 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
15:20 - 16:40 | Generic Programming and SynthesisTyDe at Aurora Borealis Chair(s): Edwin Brady University of St. Andrews, UK | ||
15:20 20mTalk | Generic Enumerators TyDe Cas van der Rest Utrecht University, Wouter Swierstra Utrecht University, Netherlands, Manuel Chakravarty Tweag I/O & IOHK Pre-print | ||
15:40 20mTalk | Generic Level Polymorphic N-ary Functions TyDe Guillaume Allais University of Strathclyde Link to publication | ||
16:00 20mTalk | Augmenting Type Signatures for Program Synthesis TyDe Pre-print | ||
16:20 20mTalk | Constraint-based Type-directed Program Synthesis TyDe Peter-Michael Osera Grinnell College Link to publication |