서브스트럭처 타입 시스템(Substructural type systems)은 별칭(aliasing)에 대해 강력한 정적 제어력을 제공합니다. 예시로는 유일성(uniqueness), 분리(separation), 그리고 차용(borrowing)이 있습니다. 이러한 제어력을 어떻게 고차 추상화, 무제한 별칭, 광범위한 공유에 의존하는 기존 언어에 가져올 수 있을까요? 우리는 Scala의 맥락에서 이 문제를 연구합니다. 우리는 전역적으로가 아니라 선택적으로 이러한 보장을 구현하는 방법을 보여줍니다: 일반 코드는 Scala의 평소 별칭 규율을 유지하며, 더 강력한 보장은 필요한 곳에서 강제될 수 있습니다. 우리의 출발점은 Scala의 캡처 검사(capture checking)이며, 이는 객체 기능성(object-capability) 전통에서 영감을 받은 기능 처리 방식을 사용합니다: 기능성은 일반 값이며, 캡처 집합(capture sets)은 값의 타입 내에서 해당 값이 사용할 수 있는 기능을 기록합니다. 우리는 이 메커니즘에 선택적 별칭 제어 계층을 추가하는 System Capybara를 개발합니다. Capybara는 기능성의 분리, 소비, 신선도, 읽기 전용 접근을 추적함으로써, 전역 불변량 없이 서브스트럭처 및 소유 기반 학문에서 핵심적인 추론 원칙들을 복구합니다. 우리는 표면 계산(surface calculus)인 Capybara에서 CoreCapybara로의 타입 보존 번역을 제공하는데, CoreCapybara는 캡처 검사의 이전 기반이었던 System Capless를 확장한 핵심 계산입니다. 이 번역은 캡처 다형성(capture polymorphism)과 신선도를 위한 한정자(quantifiers), 그리고 분리를 위한 제약 조건 인덱스 모달 타입(constraint-indexed modal types)을 사용합니다. 우리는 Lean 4에서 핵심 계산에 대한 의미론적 건전성 결과(semantic soundness result)를 증명하고, 잘 타입화된 프로그램에 대해 타입 안전성, 메모리 안전성(use-after-free 또는 double-free 없음), 읽기 전용 연산의 불변성, 그리고 데이터 레이스 자유로움을 도출합니다. 마지막으로, 우리는 Scala 3의 새로운 분리 검사기를 구현하는데, 이는 일반적인 Scala에 효과(effects), 기능성, 자원에 대한 고차 분리 추론을 가져와 공포 없는 동시성(fearless concurrency)까지 포함합니다.