A Type Theoretic Specification of Partial Evaluation
Kenichi Asai, Luminous Fennell, Peter J. Thiemann, Yang Zhang · 2014
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.