1: \begin{abstract}

2: We propose a novel method for inferring refinement types of

3: higher-order functional programs.  The main advantage of the proposed

4: method is that it can infer maximally preferred (i.e., Pareto optimal)

5: refinement types with respect to a user-specified preference order.

6: The flexible optimization of refinement types enabled by the proposed

7: method paves the way for interesting applications, such as inferring

8: most-general characterization of inputs for which a given program

9: satisfies (or violates) a given safety (or termination) property.  Our

10: method reduces such a type optimization problem to a Horn constraint

11: optimization problem by using a new refinement type system that can

12: flexibly reason about non-determinism in programs.  Our method then

13: solves the constraint optimization problem by repeatedly improving a

14: current solution until convergence via template-based invariant

15: generation.  We have implemented a prototype inference system based on

16: our method, and obtained promising results in preliminary experiments.

17: \end{abstract}

18: