A Type Theoretic Specification of Partial Evaluation
by Kenichi Asai, Luminous Fennell, Peter Thiemann, and Yang Zhang
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.
Agda Development
The Agda development of the calculus is located in this github Repository:
The code relevant to the PPDP2014 publication is in the ppdp2014
folder.
Publication
Kenichi Asai, Luminous Fennell, Peter Thiemann, and Yang Zhang
A Type Theoretic Specification of Partial Evaluation
PPDP 2014