#
A Type Theoretic Specification of Partial Evaluation

We develop a type theoretic specification of offline partial
evaluation for the simply-typed lambda calculus in the
dependently-typed programming language Agda. We establish the
correctness of the specification by proving termination, typing
preservation, and semantics preservation using logical
relations. Typing preservation is achieved by relying on a typed
syntax representation based on De Bruijn indices for the source and the
target language.
The full calculus contains primitive recursion on natural numbers and
higher-order lifting for function, product, and sum types.