# Program Synthesis from Polymorphic Refinement Types

arXiv: https://arxiv.org/abs/1510.08419 · HTML: https://mlsanity.com/paper/1510.08419/

## Key facts

- Cited by 20 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Oct 2015.

## Built on by (most cited first, 20 of 20)

- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [Top-Down Synthesis for Library Learning](https://mlsanity.com/paper/2211.16605/) (2022)
- [LILO: Learning Interpretable Libraries by Compressing and Documenting Code](https://mlsanity.com/paper/2310.19791/) (2023)
- [Neural Program Generation Modulo Static Analysis](https://mlsanity.com/paper/2111.01633/) (2021)
- [ANPL: Towards Natural Programming with Interactive Decomposition](https://mlsanity.com/paper/2305.18498/) (2023)
- [Multi-modal Program Inference: a Marriage of Pre-trainedLanguage Models and Component-based Synthesis](https://mlsanity.com/paper/2109.02445/) (2021)
- [API-guided Dataset Synthesis to Finetune Large Code Models](https://mlsanity.com/paper/2408.08343/) (2024)
- [Procedural Synthesis of Synthesizable Molecules](https://mlsanity.com/paper/2409.05873/) (2024)
- [Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems](https://mlsanity.com/paper/2605.23109/) (2026)
- [Type theory in human-like learning and inference](https://mlsanity.com/paper/2210.01634/) (2022)
- [LLM Priors for ERM over Programs](https://mlsanity.com/paper/2510.14331/) (2025)
- [P3: Joint Program-and-Proof Planning for Verified Code Generation](https://mlsanity.com/paper/2608.09277/) (2026)
- [Inductive Program Synthesis over Noisy Datasets using Abstraction Refinement Based Optimization](https://mlsanity.com/paper/2104.13315/) (2021)
- [Transformer-based Program Synthesis for Low-Data Environments](https://mlsanity.com/paper/2205.09246/) (2022)
- [VeryTrace: Verifying Reasoning Traces through Compilable Formalism and Structured Verification](https://mlsanity.com/paper/2606.24124/) (2026)
- [Refinement Type Directed Search for Meta-Interpretive-Learning of Higher-Order Logic Programs](https://mlsanity.com/paper/2102.12553/) (2021)
- [Learning to Guarantee Type Correctness in Code Generation through Type-Guided Program Synthesis](https://mlsanity.com/paper/2510.10216/) (2025)
- [Fixed-Set Robustness in Programming by Example: Example Corruption and Semantic Partition Recovery](https://mlsanity.com/paper/2607.01280/) (2026)
- [Generative Compilation: On-the-Fly Compiler Feedback as AI Generates Code](https://mlsanity.com/paper/2607.13921/) (2026)
- [Towards Certificate-Driven Software Porting: A Self-Improving Agentic Harness for Scientific Program Optimization](https://mlsanity.com/paper/2609.34069/) (2026)

## Abstract (arXiv)

We present a method for synthesizing recursive functions that provably satisfy a given specification in the form of a polymorphic refinement type. We observe that such specifications are particularly suitable for program synthesis for two reasons. First, they offer a unique combination of expressive power and decidability, which enables automatic verification---and hence synthesis---of nontrivial programs. Second, a type-based specification for a program can often be effectively decomposed into independent specifications for its components, causing the synthesizer to consider fewer component combinations and leading to a combinatorial reduction in the size of the search space. At the core of our synthesis procedure is a new algorithm for refinement type checking, which supports specification decomposition. We have evaluated our prototype implementation on a large set of synthesis problems and found that it exceeds the state of the art in terms of both scalability and usability. The tool was able to synthesize more complex programs than those reported in prior work (several sorting algorithms and operations on balanced search trees), as well as most of the benchmarks tackled by existing synthesizers, often starting from a more concise and intuitive user input.