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