UC San Diego

As software systems grow sophisticated, complex APIs are widely used to accelerate program development. However, effectively using these APIs can be challenging due to poor documentation that fails to sufficiently explain API behaviors. This issue highlights the necessity for automating the combination of APIs into programs that satisfy given high-level specifications, thereby reducing the burden on engineers.

This dissertation proposes to use type-directed program synthesis as a method for automating API navigation. In this process, the synthesizer must systematically search through APIs to construct programs that adhere strictly to the provided specifications. This task presents two primary challenges: the effective representation of these specifications and the efficient propagation of relevant information during search. To overcome these challenges, type-directed synthesis leverages compact, type-represented search spaces that enhance the propagation of type information throughout the search process. Although traditional type systems facilitate compact search space representation, they are often too coarse-grained to express user intent precisely. To address this, a semantic type system is introduced to express more advanced constraints on function signatures, effectively ruling out programs that deviate from conventional human-written code.

This dissertation provides a comprehensive analysis of type-directed program synthesis, emphasizing its advantages in handling complex API-driven environments. Through theoretical frameworks and empirical studies, it shows that type-directed synthesis techniques can solve real-world programming tasks within a reasonable time limit. The experimental results demonstrate that the developed synthesis tools significantly improve the feasibility and accuracy of synthesized programs, contributing to more efficient and reliable software development.