In this thesis, we develop an optimization technique, partial type deletion, for type checking in a polymorphic Horn clause specification. It preserves the necessary type annotations in a given program enough to guarantee the correctness of the program and delete remaining unnecessary type annotations. This technique is a generalization of Hanus' work in that Hanus' is only applied to the type general programs, whereas ours can be applied to all programs. We also present an algorithm for partial type deletion, its correctness on narrowing procedure, and finally experimental results.
본 논문에서는 폴리모픽 혼 노리 명세어의 형 검증에 있어 이를 컴파일 시에 최적화 시키는 방법에 대한 연구를 하였다. 기존의 M.Hanus의 방법이 너무 제한적이었기 때문에 이를 확장한 부분 형 제거를 제안하였고 이 방법이 정당함을 귀납적 증명을 통해 보여 주었고 실험을 통해, 기존의 방법보다 나음을 보였다.
