Synquid is a state-of-the-art program synthesizer that generates programs from refinement types, types decorated with logical predicates. One issue with this way of specifying programs is that the refinement types must be total, and thus specify what the program must do on all valid inputs. However, writing such a specification can be a burdensome task. We propose an extension of refinement specifications we call partial refinement program synthesis, where each refinement covers a partial set of the input space, but whose sum is a total specification. This will enable support for combining concrete examples and refinements in specifications will make writing specifications more accessible to non-experts. We will achieve this by introducing an intersection type to the existing refinement type synthesis method.

Michael James is a 2nd year PhD student at University of California, San Diego studying programming languages and program synthesis under Nadia Polikarpova. He worked as a software engineer for three years before starting his degree. His experience has guided him to research topics that will ultimately flow back to help other engineers and make programming easier for all.