Towards Type-Directed API Search for Mainstream Languages
summary
Claims a proof-search-based engine that treats types as specifications, supports first-class subtyping and parametric polymorphism, and translates library signatures into an internal, language-agnostic model. Implementation extracts Java APIs, stores types and type mappings for Java functional interfaces, runs backward proof search, returns multiple proofs (example: finds filter and dropWhile), and presents results in a Java prototype with web UI that currently ranks candidates by proof-tree height; code synthesis is possible but not yet scaled.
AI-written summary · about
chapters (20)
- 0:00Type-directed API search intro
- 2:07Motivation for Java API search
- 3:54Targeting mainstream languages
- 5:17Approach overview
- 7:24Source extraction model
- 9:07Query normalization proof search
- 11:34Building proof trees step-by-step
- 14:56Live demo prototype
- 16:05Future work limitations
- 17:32Key findings conclusion
- 18:15Q&A: Query language
- 20:45Q&A: Gradual typing performance
- 21:48Q&A: Language syntax
- 22:30Q&A: Extractor requirements
- 22:52Q&A: Hogle comparison
- 23:57Q&A: Swapped arguments
- 24:38Q&A: Search algorithm
- 25:18Q&A: Type mappings
- 26:21Q&A: Ranking proof trees
- 27:05Closing acknowledgments
related talks
38mType System Foundations for Super-Charged Semantic Code Search
14mTypeless Writing in a Strong Typed World
48mTDD, Like in Type Driven Development
15mLanguage-Parametric Reference Synthesis
29mType Inference Techniques: Implementation and Formalization, Better Together
26mJavaScript Tools at Scale Using Type Information
57mVariant analysis
16mDigging for Fold: Synthesis-Aided API Discovery for Haskell