이 논문에서는 정적으로 2단계 언어의 불필요한 식을 안전하게 찾는 간섭분석 방법을 제안한다. 불필요한 식이란 식의 실행이 전체 프로그램의 실행 결과에 영향을 미치지 않는 식을 말하고, 간섭분석이란 프로그램의 최종 결과에 영향을 미치는 식들을 찾아내는 분석을 말한다. 정적으로 불필요한 식을 찾으면 전체 프로그램 실행에 드는 비용을 줄일 수 있다. 이 분석은 타입 시스템에 올라탄 분석에 기반한다. 타입 규칙을 디자인하고 안전성을 증명하였으며, 이를 위한 알고리즘을 디자인하고 올바름을 증명하였다. 또한 다형 타입을 지원하도록 타입 규칙을 확장하였으며 그 안전성도 증명하였다.
This paper presents a type-based interference effect analysis for two-staged language. Non-interfering code is a subexpression whose evaluation result does not contribute to the whole program result. The analysis is based on a sound type system of multi-staged language and a type effect system. The interference effects, which are variables and indices of lambda abstractions contributing to the program result, are annotated to types and analyzed statically. We proved the soundness of the analysis. We designed a type inference algorithm constructing effects and proved its correctness.
