Synthesis from Partial Refinements
Date:
While program synthesis with refinement types as a specification is rather precise, it is not expressive enough for even some simple programs. However, synthesis with examples as a specification can be fatiguingly verbose, with some programs requiring many more examples than lines of code in the solution—rendering the synthesis a moot point.
I propose a middle ground of these two styles that offers both the expressive power of examples and the generality of refinement types. I call this style of program specification, partial refinements.
Powered by an intersection type, I will empower refinement types to include a specific example (or many) as part of the specification. I expect this to simplify the specification for some queries (like filter). Stay tuned to see this in a future conference!