일급 환경은 런타임 환경을 일반 값으로 노출하며, 치환 없는(substitution-free), 환경 기반의 운용 의미론(operational semantics)을 지원합니다. 또한 일급 모듈, 환경 조각의 동적 구성, 로컬 환경을 통한 샌드박싱과 같은 응용 프로그램도 지원합니다. 하지만 기존의 환경 기반 칼큘러스는 대부분 단순 타입 설정(simply typed setting)에서 연구되었으며 System F와 다형성(polymorphism)에 도달하지 못했습니다.
본 논문에서는 일급 환경을 가진 다형성 칼큘러스인 $F_E$를 제시합니다. 이는 작은 단계 환경 의미론(small-step environment semantics)을 통해 System F를 보존적으로 확장한 것입니다. $F_E$는 System F의 모든 형태의 치환(substitution)을 제거합니다. 항과 타입 추상화(Term and type abstractions)는 클로저(closures)로 평가되며, 박스(boxes)는 로컬 환경 하에서 코드를 실행하고, 박스 타입은 둘 다의 로컬 타입 가정(local typing assumptions)을 노출합니다.
명시적 타입(Manifest types)과 양방향 타입 동치(two-sided type equivalence)는 이중적인 역할을 수행합니다. 즉, 타입 레벨 인스턴스화(type-level instantiation)를 모델링하고 환경 및 모듈에서 투명한 타입 구성 요소를 가능하게 합니다. 우리는 타입 건전성(type soundness), 정규화(normalization), 결정 가능성(decidability), 타입 동치의 표준 속성, 그리고 System F에 대한 보존성(conservativity)을 증명합니다. $F_E$의 메타 이론은 치환 보조정리(substitution lemmas)가 아닌 인스턴스화 보조정리(instantiation lemmas)를 기반으로 합니다. 이 기초는 동적 구성과 샌드박싱이 가능한 다형성 일급 모듈을 지원합니다.
우리는 $F_E$를 두 가지 형태로 연구합니다. 주요 발표 내용은 기존 System F를 따르는 명시적 타입 전달 칼큘러스입니다. 또한, 우리는 다형 함수형 언어의 의미론에 맞춰진 암묵적으로 타입 지정된 변형체(implicitly-typed variant)도 개발했습니다. 모든 메타 이론은 Rocq 증명기(theorem prover)에서 기계화되었습니다.