# OOPSLA24 Response

We appreciate the insightful feedback provided by the anonymous reviewers. Below, we address some of the main concerns and questions.

**Relationship with Previous Work:** The expressiveness of the original abstract refinement work [1] is limited by the positions in which abstract predicates can appear (e.g., they cannot be placed under a disjunction). Consequently, more complex cases, such as those in STORM [2], are only expressible with bounded refinements [3]. On the other hand, Economou et al. [4] only considered base-sorted parameters. Our work demonstrates how the simple syntactic inference of Economou et al. can be extended to function-sorted parameters, allowing us to express many examples that previously required complicated bounds. Further, index generics come with their own restrictions (e.g., they must appear in positions where they can be unified), this creates a trade-off between constraint and index generics. Our work shows how they can be combined in the same system, providing two methods for inferring refinement parameters.

**Formalism and Proofs:** The main theoretical contribution is the formalization of the algorithmic system, which shows how to instantiate parameters in a system that combines index and constraint generics. This represents an improvement over [1], which *did not* formalize inference and only defined a language where refinement parameters are explicitly instantiated. We have adapted the semantic argument and translation into the polymorphic calculus from [1], and we expect the proofs to be similar and mostly standard. However, we have not yet completed the proofs.

**Relationship to Rust:** Our approach is largely orthogonal to Rust and can be applied to other systems (e.g., Liquid Haskell). A notable difference is that, since Rust is an imperative language, indices are necessary to have a pure language of refinements. Thus, the machinery developed for Flux makes it straightforward to support function-sorted generic refinements.

[1] Vazou, Niki, Patrick M. Rondon, and Ranjit Jhala. "Abstract refinement types." European Symposium on Programming. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013.

[2] Lehmann, N., Kunkel, R., Brown, J., Yang, J., Vazou, N., Polikarpova, N., Stefan, D. and Jhala, R., 2021. STORM: Refinement types for secure web applications. In 15th USENIX Symposium on Operating Systems Design and Implementation.

[3] Vazou, Niki, Alexander Bakst, and Ranjit Jhala. "Bounded refinement types." Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming. 2015.

[4] Economou, Dimitrios J., Neel Krishnaswami, and Jana Dunfield. "Focusing on refinement typing." ACM Transactions on Programming Languages and Systems