최근 도입된 종속 타입 고차 논리(DHOL)는 표현력과 자동화 지원 간의 흥미로운 절충안을 제공합니다. 표준 HOL보다 표현력을 크게 확장하기 위해 타입 시스템의 결정 가능성을 희생하지만, HOL로의 정확하고 완전한 변환을 통해 강력한 자동 정리 증명 지원을 유지합니다. 본 논문에서는 이러한 설계를 활용하여 DHOL에 정제 타입과 몫 타입을 확장합니다. 이 두 가지는 실무자들이 일반적으로 요청하지만 자동 정리 증명기에서 거의 제공되지 않습니다. 이는 본질적으로 결정 불가능한 타이핑을 필요로 하므로 결정 가능한 타입 시스템에 역으로 적용하기가 매우 어렵기 때문입니다. 그러나 DHOL이 이미 어려운 작업을 처리하고 있으므로, 이들을 추가하는 것은 가능할 뿐만 아니라 우아하고 간단합니다. 구체적으로, 하위 타입의 특수한 경우로 정제 타입과 몫 타입을 추가합니다. 이는 관련된 정준 포함 또는 투영 맵을 항등 맵으로 바꾸어 표현 방식의 비용이 많이 드는 변경을 방지합니다. 확장된 언어에 대한 구문, 의미론 및 HOL로의 변환과 함께 정확성 및 완전성 증명을 제시합니다.
