Refinement Type Inference via Horn Constraint Optimization

TL;DR

This paper introduces a new approach for inferring optimal refinement types in higher-order functional programs by formulating and solving Horn constraint optimization problems, enabling flexible and precise program property analysis.

Contribution

It presents a novel method that infers Pareto optimal refinement types using Horn constraint optimization and a new refinement type system for non-determinism.

Findings

Successfully infers maximally preferred refinement types

Enables characterization of input conditions for safety and termination

Prototype implementation shows promising preliminary results

Abstract

We propose a novel method for inferring refinement types of higher-order functional programs. The main advantage of the proposed method is that it can infer maximally preferred (i.e., Pareto optimal) refinement types with respect to a user-specified preference order. The flexible optimization of refinement types enabled by the proposed method paves the way for interesting applications, such as inferring most-general characterization of inputs for which a given program satisfies (or violates) a given safety (or termination) property. Our method reduces such a type optimization problem to a Horn constraint optimization problem by using a new refinement type system that can flexibly reason about non-determinism in programs. Our method then solves the constraint optimization problem by repeatedly improving a current solution until convergence via template-based invariant generation. We have implemented a prototype inference system based on our method, and obtained promising results in preliminary experiments.