지난 20년 동안 수많은 시스템들이 의존 타입(dependent typing)의 여러 이점을 다양한 새로운 프로그래밍 언어에 도입해 왔으며, 종종 타입을 내부에서 어떤 항이 나타날 수 있는지 제한하는 방식으로 이루어졌습니다. 이러한 기법들은 정제 타입(refinement types), 발생 타입(occurrence typing), 리퀴드 타입(liquid types), 경로 의존 타입(path dependent types) 등으로 알려져 있습니다. 하지만 이 시스템들이 채택한 제약 조건들은 종종 치환 속성(substitution property)을 깨뜨립니다. 왜냐하면 이러한 제약은 타입 내부의 변수에 임의의 항을 치환하는 능력을 명시적으로 금지하기 때문입니다. 이는 이러한 시스템들의 설계와 메타 이론에 상당한 복잡성을 야기하며, 중대한 오류가 발생할 가능성을 증가시킵니다. 우리는 발생 타입에 관한 특정 연구 흐름, 즉 Tobin-Hochstadt과 Felleisen이 2010년에 발표한 Typed Racket의 근간을 이루는 계산(calculus)에 주목합니다. 우리는 타입 내부로의 치환이라는 근본적인 어려움이 이 작업의 형식주의와 구문적 타입 건전성 정리(syntactic type soundness theorem)에 여러 결함을 초래했음을 보여줍니다. 이러한 결함들은 이 작업을 기반으로 하는 여러 다른 논문들에서도 재현되며, Typed Racket 자체에서도 건전성 버그로 나타납니다. 우리는 이러한 문제점들을 식별하고 수정함으로써 Typed Racket의 핵심 계산을 개정하고, Lean에 형식화된 단계 인덱스 논리 관계(step-indexed logical relations)를 사용하여 extit{의미론적 타입 건전성}(semantic type soundness) 증명을 제공합니다. 우리는 이 접근 방식이 보이는 것보다 간단하며, Typed Racket의 발생 타입을 처리하는 복잡성을 쉽게 확장할 수 있다고 주장합니다.