Agda formalization of PEPM 2019 paper
December 8, 2018
This page contains the
Agda formalization of the paper:
"Extracting a Call-by-Name Partial Evaluator from a Proof of
ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based
Program Manipulation (PEPM 2019), 7 pages, to appear (January 2019).
tested on Agda 2.5.2, standard library 0.13
- all the following files in
types, terms, renaming, substitution
Andreas Abel's formalization.
- reduction relation for weak reduction
- termination proof for weak reduction
- reduction/equality relation for strong reduction
- termination proof for strong reduction
This document was translated from LATEX by