Specifying the Semantics of Program Specialization using Type Theory

Peter Thiemann, University of Nottingham

We define the static semantics of program
specialization for the simply-typed lambda calculus using a
translation into a suitable Martin-Loef-style type theory.
The translation provides a framework in which to compare different
specializers. Our approach reveals that the distinction between
specialization-time and run-time computation is related to the
compile-time vs. run-time phase distinction in type theory.