정제 타입 (Refinement types)은 사용하기 쉽고 자연스러우면서도, 전통적인 타입 시스템 (type systems)의 표현력을 높이는 것을 목표로 하는 정적 검증 (static verification) 기술입니다. 정제 타입을 기반으로 하는 시스템들이 여러 주류 언어들을 위해 개발되어 왔지만, 이들의 실질적인 채택은 어노테이션 오버헤드 (annotation overhead)로 인해 여전히 제한적입니다. 이러한 오버헤드는 Java나 Scala와 같은 언어의 "일반적인" 타입 어노테이션을 사용할 때보다 종종 더 큰 부담이 됩니다. 최신 기술 수준을 개선하기 위해, 본 논문은 Ranger를 소개합니다. Ranger는 어노테이션 오버헤드를 작게 유지하고 변수(variables) 및 루프(loops)와 같은 명령형 스타일의 구조 (imperative-style constructs)와 원활하게 통합되도록 설계된 정제 타입 시스템입니다. 이름에서 알 수 있듯이, Ranger는 정수 범위 타입 (integer range types)에 집중합니다. 이는 유계된 정수 범위 (bounded integer ranges)를 표현하는 특수한 종류의 정제 타입입니다. 이러한 타입은 올바른 인덱스 조작 (index manipulation) 및 범위 내 데이터 접근 (in-bounds data accesses) 등을 검증하는 데 널리 유용합니다. 표현력과 간결함을 결합하기 위해, Ranger는 양방향 타입 시스템 (bidirectional type system)을 기반으로 하며, 이는 타입 추론 (type inference) 알고리즘을 실행하여 타입 체크 (typechecking) 단계에서 사용자가 직접 작성해야 하는 보조 어노테이션 (auxiliary annotations)의 필요성을 줄이는 데 유용한 정보를 제공합니다. 또한 Ranger는 명시적인 어노테이션 없이도 프로그램의 동작을 정밀하게 포착하는 다른 형태의 경량 흐름 민감형 정적 분석 (lightweight flow-sensitive static analysis) 기술들을 통합합니다. 우리는 Licorne 실험적 프로그래밍 언어 위에 Ranger를 구현했습니다. 우리의 실험 결과에 따르면, Ranger의 구현은 Java 및 Scala와 같은 표준 정적 타입 시스템의 능력을 벗어나는 다양한 유용한 속성들을 간결하게 표현하고 검증할 수 있으며, 범위에 관한 속성을 검사할 수 있는 Java Checker Framework 및 Liquid Java와 같은 다른 확장된 타입 시스템들과 비교해도 우수한 성능을 보입니다.