The following summary was generated by AI from the slides.
Type-Based Resource-Guided Search uses resource type information inferred by Automatic Amortized Resource Analysis (AARA) — as implemented in tools such as RaML, which assigns append the type encoding a bound of — to guide program synthesis search toward candidates that satisfy both functional specifications and complexity constraints. Static resource analysis derives sound, modular, compile-time worst-case bounds over all inputs, enabling detection of complexity regressions (e.g., escalating to when a nested call is introduced) as demonstrated with Facebook’s Infer cost checker. By making AARA-derived resource bounds a first-class component of the synthesis search procedure, the approach avoids the incomplete coverage and high overhead of purely performance-test-driven synthesis.