Type Directed Partial Evaluation for Level-1 Shift and Reset

TL;DR

This paper implements type directed partial evaluation algorithms for shift and reset control operators in Coq, proving their correctness and normal form transformation capabilities within a dependently typed semantic framework.

Contribution

It introduces a novel TDPE algorithm for shift/reset with strong sum types, validated in Coq, and demonstrates its ability to normalize programs beyond existing equational theories.

Findings

Algorithm transforms well-typed programs to normal forms

Normal forms not achievable by known equational theories

Semantic domain uses dependently typed monadic structures

Abstract

We present an implementation in the Coq proof assistant of type directed partial evaluation (TDPE) algorithms for call-by-name and call-by-value versions of shift and reset delimited control operators, and in presence of strong sum types. We prove that the algorithm transforms well-typed programs to ones in normal form. These normal forms can not always be arrived at using the so far known equational theories. The typing system does not allow answer-type modification for function types and allows delimiters to be set on at most one atomic type. The semantic domain for evaluation is expressed in Constructive Type Theory as a dependently typed monadic structure combining Kripke models and continuation passing style translations.