Type Directed Partial Evaluation for Level-1 Shift and Reset

Danko Ilik

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.

In Ugo de'Liguoro and Alexis Saurin: Proceedings First Workshop on Control Operators and their Semantics (COS 2013), Eindhoven, The Netherlands, June 24-25, 2013 , Electronic Proceedings in Theoretical Computer Science 127, pp. 86–100.
Published: 4th September 2013.

ArXived at: https://dx.doi.org/10.4204/EPTCS.127.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org