pith. sign in

arxiv: 2607.00824 · v1 · pith:GJRQDI3Snew · submitted 2026-07-01 · 💻 cs.PL

Practical Range Refinement Types with Inference

Valentin Aebi , Carlo A. Furia This is my paper

Pith reviewed 2026-07-02 01:52 UTC · model grok-4.3

classification 💻 cs.PL
keywords refinement typesrange typestype inferenceflow-sensitive analysisimperative programmingbounds checkingstatic verification
0
0 comments X

The pith

Ranger's bidirectional inference and flow analysis verify integer range properties in imperative code with low annotation overhead.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents Ranger as a refinement type system specialized for integer ranges to check properties like index bounds and in-bounds accesses. It pairs a bidirectional type system with flow-sensitive analysis so that inference supplies most of the information needed for verification and thereby keeps user annotations small. Experiments on the Licorne language show that the system can express and check a range of useful properties that standard type systems in Java or Scala cannot handle. Ranger is also shown to require fewer annotations than the Java Checker Framework or Liquid Java when performing similar checks. A sympathetic reader would care because this combination could make refinement-based verification practical for everyday imperative code that manipulates arrays and loops.

Core claim

Ranger is a refinement type system for bounded integer ranges that integrates with imperative constructs such as variables and loops; it relies on a bidirectional type inference algorithm together with lightweight flow-sensitive static analysis to reduce the need for explicit annotations while still verifying properties such as correct index manipulation and in-bounds data accesses, as demonstrated by its implementation on Licorne and the reported experiments.

What carries the argument

Bidirectional type inference algorithm combined with flow-sensitive static analysis techniques for range properties.

If this is right

  • Ranger can express and verify properties such as correct index manipulation that fall outside standard static type systems.
  • The system integrates directly with imperative-style code including variables and loops.
  • Ranger requires fewer annotations than the Java Checker Framework or Liquid Java for comparable range checks.
  • Experiments confirm that the approach works on a variety of range-related verification tasks in the Licorne language.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same inference-plus-flow-analysis pattern could be applied to other refinement properties beyond integer ranges.
  • If the low-annotation claim holds, languages with built-in range checking might adopt similar inference to reduce programmer burden.
  • The favorable comparison suggests that targeted refinement systems may be more practical than general-purpose ones for common safety properties.

Load-bearing premise

The inference algorithm and flow analysis can precisely capture program behavior for range properties without explicit user annotations in the majority of cases.

What would settle it

A concrete program containing loops or variable updates on array indices where Ranger still demands a large number of manual annotations to verify an in-bounds property that the abstract claims can be handled concisely.

Figures

Figures reproduced from arXiv: 2607.00824 by Carlo A. Furia, Valentin Aebi.

Figure 1
Figure 1. Figure 1: Motivating example. 4 [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The syntax of IRcorne, licorne’s intermediate representation. Vars stands for the set of program variables, each corresponding to a uniquely defined value in SSA form; Preds for the set of predicate identifiers (pure functions that return Bool), Classes for the set of user-defined types, and Z for the set of integer numbers. Nothing and Any are the bottom and top types. fn maxPos(a: Array[Int]) →[0 ..] { v… view at source ↗
Figure 3
Figure 3. Figure 3: Function maxPos returns the largest non-negative element in array a, or zero if all elements of a are negative. an error). A conditional if 𝑐 then 𝑡 else 𝑒 merge 𝑚 next 𝑛 introduces of two blocks 𝑡 and 𝑒, one of which executes depending on the Boolean condition 𝑐; in addition, a sequence 𝑚 of 𝜙 functions merge the variables defined in the two branches; and 𝑛 declares the block executed afterwards. A loop f… view at source ↗
Figure 4
Figure 4. Figure 4: ranger’s typing rules. 10 [PITH_FULL_IMAGE:figures/full_fig_p010_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: An overview of ranger’s typechecking workflow. refinements) and the corresponding numeric variables are only linearly updated, then the constraints are in integer linear arithmetic, which is NP complete. Despite these worst-case bounds, as confirmed in Sec. 5’s experiments, ranger’s typechecking is fast on “natural” programs. In addition, ranger’s implementation reduces the complexity of the constraints th… view at source ↗
read the original abstract

Refinement types are a static verification technique that aims at increasing the expressivity of traditional type systems while remaining easy and natural to use. While systems based on refinement types have been developed for several mainstream languages, their practical adoption remains limited by their annotation overhead, which is often a more significant burden than when using the "plain" type annotations of languages like Java or Scala. To improve the state of the art, this paper introduces Ranger: a refinement type system designed to keep the annotation overhead small and to seamlessly integrate with imperative-style constructs like variables and loops. As the name suggests, Ranger focuses on integer range types: a particular kind of refinement types that express bounded integer ranges. Such types are widely useful to verify correct index manipulation and in-bounds data accesses, among others. To combine expressiveness and succinctness, Ranger is based on a bidirectional type system, which runs a type inference algorithm to provide the typechecking pass with information useful to reduce the need for user-written auxiliary annotations. Ranger also integrates other forms of lightweight flow-sensitive static analysis techniques that precisely capture the program's behavior without explicit annotations. We implemented Ranger on top of the Licorne experimental programming language. Our experiments show that Ranger's implementation can concisely express and verify a variety of useful properties that fall beyond the capabilities of standard static type systems like those of Java and Scala, and that Ranger compares favorably to other extended type systems, such as the Java Checker Framework and Liquid Java, that can also check properties about ranges.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper presents Ranger, a refinement type system for integer range properties in imperative code. It combines a bidirectional type system with type inference and lightweight flow-sensitive analysis to minimize annotations, implemented atop the Licorne language. Experiments are claimed to show that Ranger concisely expresses and verifies range properties beyond standard Java/Scala types and compares favorably to the Java Checker Framework and Liquid Java.

Significance. If the implementation details, inference algorithm, and experimental results hold, the work could advance practical adoption of refinement types for a common class of properties (integer ranges) by addressing annotation overhead, a known barrier in the field.

major comments (2)
  1. [Abstract] Abstract: the central empirical claims rest on 'experiments' demonstrating concise expression, verification success, and favorable comparisons, yet the abstract (and provided description) supplies no information on type rules, inference algorithm correctness, benchmark programs, annotation counts, or evaluation methodology; these details are load-bearing for assessing whether the weakest assumption (precise capture of imperative behavior without most annotations) holds.
  2. No section or equation is supplied that defines the bidirectional inference rules or proves soundness of the range refinement system; without this, the claim that the system 'precisely capture[s] the program's behavior' cannot be evaluated for internal consistency or edge cases in loops and mutation.
minor comments (1)
  1. [Abstract] The abstract could more explicitly state the scope of properties handled (e.g., whether only simple bounds or also relations between variables).

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their comments on the manuscript. We respond to each major comment below.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the central empirical claims rest on 'experiments' demonstrating concise expression, verification success, and favorable comparisons, yet the abstract (and provided description) supplies no information on type rules, inference algorithm correctness, benchmark programs, annotation counts, or evaluation methodology; these details are load-bearing for assessing whether the weakest assumption (precise capture of imperative behavior without most annotations) holds.

    Authors: The abstract follows standard conventions for brevity. The full manuscript details the bidirectional type system and inference algorithm in Sections 3 and 4, while Section 5 describes the benchmark programs, annotation counts, evaluation methodology, and comparisons to the Java Checker Framework and Liquid Java. We will revise the abstract to include a brief reference to the experimental evaluation. revision: yes

  2. Referee: [—] No section or equation is supplied that defines the bidirectional inference rules or proves soundness of the range refinement system; without this, the claim that the system 'precisely capture[s] the program's behavior' cannot be evaluated for internal consistency or edge cases in loops and mutation.

    Authors: The manuscript describes the bidirectional type system, inference algorithm, and flow-sensitive analysis in Sections 3 and 4 using textual explanations and examples, without formal equations or a soundness proof. This reflects the paper's practical focus on implementation in Licorne and empirical results rather than theoretical foundations. The claims regarding precise capture of program behavior are supported by the experiments; a formal proof is outside the intended scope. revision: no

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper presents Ranger as an implemented refinement type system whose claims of low annotation overhead, expressiveness for range properties, and favorable comparisons rest on concrete implementation details and reported experiments rather than any closed mathematical derivation. No equations, predictions, or uniqueness theorems are described that reduce by construction to fitted inputs or self-citations; the bidirectional inference and flow-sensitive analysis are design choices justified by the resulting system behavior, not by internal redefinition. The central claims are therefore empirically grounded and self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Abstract-only review; no free parameters, invented entities, or non-standard axioms are described. The work relies on standard assumptions from refinement type literature about soundness of type systems and the feasibility of inference for imperative constructs.

axioms (1)
  • domain assumption Refinement types for integer ranges can be integrated with imperative constructs (variables, loops) while preserving practical usability and soundness.
    Invoked implicitly by the design goals stated in the abstract for seamless integration with imperative-style code.

pith-pipeline@v0.9.1-grok · 5793 in / 1401 out tokens · 32762 ms · 2026-07-02T01:52:28.647294+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

35 extracted references · 22 canonical work pages

  1. [1]

    Master’s thesis, EPFL, Lausanne, Switzerland (January 2025), available athttps://valentinaebi.g ithub.io/resources/ms-thesis.pdf

    Aebi, V.: Implementation of a gradually compartmentalized programming language. Master’s thesis, EPFL, Lausanne, Switzerland (January 2025), available athttps://valentinaebi.g ithub.io/resources/ms-thesis.pdf

    2025

  2. [2]

    ACM SIGPLAN Notices33(4), 17–20 (1998)

    Appel, A.W.: SSA is functional programming. ACM SIGPLAN Notices33(4), 17–20 (1998). https://doi.org/10.1145/278283.278285

    work page doi:10.1145/278283.278285 1998

  3. [3]

    Brady, E.: Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Program.23(5), 552–593 (2013).https://doi.org/10.1017/S0 95679681300018X

    work page doi:10.1017/s0 2013

  4. [4]

    In: Symposium on Automatic Demonstration

    de Bruijn, N.G.: The mathematical language AUTOMATH, its usage, and some of its extensions. In: Symposium on Automatic Demonstration. Lecture Notes in Mathematics, vol. 125, pp. 29–61. Springer (1970).https://doi.org/10.1007/BFb0060623

    work page doi:10.1007/bfb0060623 1970

  5. [5]

    In: Proc

    Callaú,O.,Robbes,R.,Tanter,E.,Röthlisberger,D.,Bergel,A.:Ontheuseoftypepredicatesin object-oriented software: The case of Smalltalk. In: Proc. 10th ACM Symposium on Dynamic Languages. pp. 135–146. ACM (2014).https://doi.org/10.1145/2661088.2661091

    work page doi:10.1145/2661088.2661091 2014

  6. [6]

    The Checker Framework manual: Custom pluggable types for Java.https://checkerframe work.org/manual/, last accessed 2026/06/27

    2026

  7. [7]

    Coquand, T., Huet, G.P.: The calculus of constructions. Inf. Comput.76(2/3), 95–120 (1988). https://doi.org/10.1016/0890-5401(88)90005-3

    work page doi:10.1016/0890-5401(88)90005-3 1988

  8. [8]

    In: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977

    Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977. pp. 238–252. ACM (1977).https://doi.org/10.1145/512950.512973

    work page doi:10.1145/512950.512973 1977

  9. [9]

    ACM Comput

    Dunfield, J., Krishnaswami, N.: Bidirectional typing. ACM Comput. Surv.54(5), 98:1–98:38 (jun 2021).https://doi.org/10.1145/3450952

    work page doi:10.1145/3450952 2021

  10. [10]

    In: Proc

    Flanagan, C.: Hybrid type checking. In: Proc. 33rd ACM SIGPLAN-SIGACT Symposium on PrinciplesofProgrammingLanguages,POPL2006,Charleston,SouthCarolina,USA,January 11-13, 2006. pp. 245–256. ACM (2006).https://doi.org/10.1145/1111037.1111059

    work page doi:10.1145/1111037.1111059 2006

  11. [11]

    In: International Conference on Parallel Problem Solving from Nature

    Fonseca, A., Santos, P., Silva, S.: The usability argument for refinement typed genetic programming. In: International Conference on Parallel Problem Solving from Nature. pp. 18–32. Springer (2020)

    2020

  12. [12]

    SIGPLAN Not.26(6), 268–277 (jun 1991).https://doi.org/10.1145/113446.113468

    Freeman, T., Pfenning, F.: Refinement types for ML. SIGPLAN Not.26(6), 268–277 (jun 1991).https://doi.org/10.1145/113446.113468

    work page doi:10.1145/113446.113468 1991

  13. [13]

    Furia, C.A.: Software analysis course at USI: course material.https://github.com/bugco unting/software-analysis/

  14. [14]

    In: Proc

    Gamboa, C., Canelas, P., Timperley, C., Fonseca, A.: Usability-oriented design of liquid types for Java. In: Proc. 45th International Conference on Software Engineering (ICSE ’23). pp. 1520–1532. IEEE Press (2023).https://doi.org/10.1109/ICSE48619.2023.00132

    work page doi:10.1109/icse48619.2023.00132 2023

  15. [15]

    In: Lindley, S., McBride, C., Trinder, P.W., Sannella, D

    Jones, S.P., Weirich, S., Eisenberg, R.A., Vytiniotis, D.: A reflection on types. In: Lindley, S., McBride, C., Trinder, P.W., Sannella, D. (eds.) A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. pp. 292–317. Lecture Notes in Computer Science, Springer (2016).https://doi.org/10.1007/97...

    work page doi:10.1007/978-3-3 2016

  16. [16]

    In: International Conference on Verification, Model Checking, and Abstract Interpretation

    Kazerounian,M.,Vazou,N.,Bourgerie,A.,Foster,J.S.,Torlak,E.:RefinementtypesforRuby. In: International Conference on Verification, Model Checking, and Abstract Interpretation. pp. 269–290. Springer International Publishing, Cham (dec 2017)

    2017

  17. [17]

    In: Proc

    Kellogg, M., Dort, V., Millstein, S., Ernst, M.D.: Lightweight verification of array indexing. In: Proc. 27th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2018). pp. 3–14. Association for Computing Machinery, New York, NY, USA (2018). https://doi.org/10.1145/3213846.3213849 17

    work page doi:10.1145/3213846.3213849 2018

  18. [18]

    Springer, 2nd edn

    Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Springer, 2nd edn. (2016).https://doi.org/10.1007/978-3-662-50497-0

    work page doi:10.1007/978-3-662-50497-0 2016

  19. [19]

    Lehmann, N., Geller, A.T., Vazou, N., Jhala, R.: Flux: Liquid types for Rust. Proc. ACM Program. Lang.7(PLDI), 169:1–169:25 (jun 2023).https://doi.org/10.1145/3591283

    work page doi:10.1145/3591283 2023

  20. [20]

    Liquidjava - Extending Java with Liquid Types, GitHub repository.https://github.com/l iquid-java/liquidjava, last accessed 2026/06/21

    2026

  21. [21]

    LiquidJava examples, GitHub repository.https://github.com/liquid-java/liquidjava -examples, last accessed 2026/05/20

    2026

  22. [22]

    Open VSX page of the LiquidJava Visual Studio Code extension.https://open-vsx.org/e xtension/AlcidesFonseca/liquid-java, last accessed 2026/06/21

    2026

  23. [23]

    Martin-Löf, P.: Intuitionistic type theory, Studies in proof theory, vol. 1. Bibliopolis (1984)

    1984

  24. [24]

    In: Tools and Algorithms for the Construction and Analysis of Systems

    de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2008. Lecture Notes in Computer Science, vol. 4963. Springer, Berlin, Heidelberg (2008).https://doi.org/10.1007/978-3-540-788 00-3_24

    work page doi:10.1007/978-3-540-788 2008

  25. [25]

    In: Proc

    Papi, M.M., Ali, M., Correa, T.L., Perkins, J.H., Ernst, M.D.: Practical pluggable types for Java. In: Proc. 2008 International Symposium on Software Testing and Analysis (ISSTA ’08). pp. 201–212. Association for Computing Machinery, New York, NY, USA (2008). https://doi.org/10.1145/1390630.1390656

    work page doi:10.1145/1390630.1390656 2008

  26. [26]

    The MIT Press (2002)

    Pierce, B.C.: Types and Programming Languages. The MIT Press (2002)

    2002

  27. [27]

    https://github.com/plume- lib/plume- util , last accessed 2026/06/21

    Plume documentation. https://github.com/plume- lib/plume- util , last accessed 2026/06/21

    2026

  28. [28]

    In: International Conference on Computer Aided Verification

    Rondon, P., Bakst, A., Kawaguchi, M., Jhala, R.: Csolve: Verifying C with liquid types. In: International Conference on Computer Aided Verification. pp. 744–750. Springer Berlin Heidelberg, Berlin, Heidelberg (jul 2012)

    2012

  29. [29]

    In: Proc

    Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: Proc. 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’08). pp. 159–169. Association for Computing Machinery, New York, NY, USA (2008).https://doi.org/10.1 145/1375581.1375602

    work page arXiv 2008

  30. [30]

    In: Proc

    Schmid, G.S., Kuncak, V.: SMT-based checking of predicate-qualified types for Scala. In: Proc. 2016 7th ACM SIGPLAN Symposium on Scala (SCALA 2016). pp. 31–40. Association for Computing Machinery, New York, NY, USA (2016).https://doi.org/10.1145/299839 2.2998398

    work page doi:10.1145/299839 2016

  31. [31]

    https://github.com/TheAlgorithms/Java , last accessed 2026/06/21

    The Algorithms - Java. https://github.com/TheAlgorithms/Java , last accessed 2026/06/21

    2026

  32. [32]

    In: Proc

    Tobin-Hochstadt, S., Felleisen, M.: Logical types for untyped languages. In: Proc. 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010. pp. 117–128. ACM (2010).https://doi.org/10 .1145/1863543.1863561

    work page arXiv 2010

  33. [33]

    Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton-Jones, S.: Refinement types for Haskell.In:Proc.19thACMSIGPLANInternationalConferenceonFunctionalProgramming (ICFP ’14). pp. 269–282. Association for Computing Machinery, New York, NY, USA (2014). https://doi.org/10.1145/2628136.2628161

    work page doi:10.1145/2628136.2628161 2014

  34. [34]

    In: Proc

    Vekris, P., Cosman, B., Jhala, R.: Refinement types for TypeScript. In: Proc. 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16). pp. 310–325. Association for Computing Machinery, New York, NY, USA (2016).https: //doi.org/10.1145/2908080.2908110

    work page doi:10.1145/2908080.2908110 2016

  35. [35]

    Willsey, M., Nandi, C., Wang, Y.R., Flatt, O., Tatlock, Z., Panchekha, P.: egg: Fast and extensible equality saturation. Proc. ACM Program. Lang.5(POPL), 1–29 (2021).https: //doi.org/10.1145/3434304,https://doi.org/10.1145/3434304 18

    work page doi:10.1145/3434304 2021