추상 해석 (Abstract Interpretations)으로서의 효과 시스템 (Effect Systems)

프로그램 동작에 대한 정적 추론 (static reasoning)의 많은 형태가 문헌에 알려져 있지만, 이들 사이의 형식적 관계 (formal relationships)는 놀라울 정도로 드물게 연구되고 있습니다. 대부분의 타입 시스템 (type systems)이 추상 해석 (abstract interpretations)에 의해 포착된다는 점은 잘 알려져 있지만, 타입-및-효과 시스템 (type-and-effect systems)의 경우, 효과 시스템을 추상 해석으로 프레이밍 (framing)하는 강력한 가설과 간헐적인 시도에도 불구하고 일반적인 사례에서는 아직 확정되지 않은 상태입니다. 우리는 추상 해석 (abstract interpretations)과 일반적인 클래스의 효과 시스템 (effect systems) 사이의 형식적 관계를 개발합니다. 첫째, 효과 콴탈 (effect quantales)을 추상 도메인 (abstract domains)으로 임베딩 (embedding)하는 방법을 설명합니다. 둘째, 효과 콴탈 (effect quantale)의 일반적인 형태를 추상 해석 (abstract interpretation)으로서 복구합니다. 이는 상태 (states)나 값 (values)에 대한 것이 아니라, 이벤트 발생 (event occurrences)에 대한 것입니다.