Posts by Collection

portfolio

publications

Program Synthesis by Type-Guided Abstraction Refinement

Published in Principles of Programming Languages 2020, 2019

We consider the problem of type-directed component based synthesis where, given a set of (typed) components and a query type, the goal is to synthesize a term that inhabits the query. Classical approaches based on proof search in intuitionistic logics do not scale up to the standard libraries of modern languages, which span hundreds or thousands of components. Recent graph reachability based methods proposed for languages like Java do scale, but only apply to components over monomorphic data and functions: polymorphic data and functions infinitely explode the size of the graph that must be searched, rendering synthesis intractable. We introduce type-guided abstraction refinement (TYGAR), a new approach for scalable type-directed synthesis over polymorphic datatypes and components. Our key insight is that we can overcome the explosion by building a graph over abstract types which represent a potentially unbounded set of concrete types. We show how to use graph reachability to search for candidate terms over abstract types, and introduce a new algorithm that uses proofs of untypeability of ill-typed candidates to iteratively refine the abstraction until a well-typed result is found.

Recommended citation: Guo, Z. (2019). "Program Synthesis by Type-Guided Abstraction Refinement." POPL 2020. 1(1). http://michaelbjames.com/files/tygar-2020.pdf

Digging for Fold: Synthesis-Aided API Discovery for Haskell

Published in OOPSLA 20, 2020

We present Hoogle+, a web-based API discovery tool for Haskell. A Hoogle+ user can specify a programming task using either a type, a set of input-output tests, or both. Given a specification, the tool returns a list of matching programs composed from functions in popular Haskell libraries, and annotated with automatically-generated examples of their behavior. These features of Hoogle+ are powered by three novel techniques. First, to enable efficient type-directed synthesis from tests only, we develop an algorithm that infers likely type specifications from tests. Second, to return high-quality programs even with ambiguous specifications, we develop a technique that automatically eliminates meaningless and repetitive synthesis results. Finally, we show how to extend this elimination technique to automatically generate informative inputs that can be used to demonstrate program behavior to the user. To evaluate the effectiveness of Hoogle+ compared with traditional API search techniques,we perform a user study with 30 participants of varying Haskell proficiency. The study shows that programmers equipped with Hoogle+ generally solve tasks faster and were able to solve 50% more tasks overall.

Recommended citation: James, M. (2020). "Digging for Fold: Synthesis-Aided API Discovery for Haskell." OOPSLA 2020. 1(1). http://michaelbjames.com/files/digging-for-fold.pdf

talks

Component-based Type-driven Synthesis

Published:

I discussed Hoogle+, one of my research projects. It is a component-based type-driven synthesis technique for Haskell. Relying on a library of everyday functions and an input type query, the system finds an inhabitant of the, potentially polymorphic, type using those provided component set. The search tames an explosion of infinite types through a novel type-guided abstraction refinement (TYGAR) approach.

Synthesis from Partial Refinements

Published:

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.

Interaction Modalities in Program Synthesis

Published:

Program synthesis searches from a high level specification to find a program that matches a user’s intent. Interactive program synthesis considers the human an essential part of that search process. Providing interactions comes in largely two forms: there are interactions that serve to get information into the system and those that get information out from the synthesizer. In some synthesizers, that output information also works to solicit new information which in turn refines the search, making for an interaction loop with the synthesizer. In this work, I classify interactions to gather information into, out of, and form loops of synthesis systems while fitting my ongoing work into this research landscape. I look at this interaction loop in the context of interaction theory. I conclude by highlighting open questions and areas for improvement in search interactions.

teaching

Undergraduate Teaching Assistant

COMP 105 - Programming Languages, Tufts University, 2015

Teaching Assistant for Kathleen Fisher’s programming languages course. I led a weekly recitation for students to better understand the semantic differences between imperative and functional programming languages. I helped to grade student homework assignments and tests.

Graduate Teaching Assistant

CSE130 - Programming Languages, University California, San Diego, 2019

Teaching Assistant for Nadia Polikarpova’s programming languages course. I ran a discussion section to reinforce knowledge on the Haskell programming language and run test-prep. As with any course, I held office hours, graded assignments/exams, and tended the garden of Piazza questions.