Agda formalization of PEPM 2019 paper

Kenichi Asai

December 8, 2018

Abstract: This page contains the Agda formalization of the paper:

Asai, K. "Extracting a Call-by-Name Partial Evaluator from a Proof of Termination," ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM 2019), 7 pages, to appear (January 2019).

Contents

• tested on Agda 2.5.2, standard library 0.13
• all the following files in zip

deBruijn-cbn.agda

types, terms, renaming, substitution based on Andreas Abel's formalization.

reduce-cbn.agda

reduction relation for weak reduction

normal-cbn.agda

termination proof for weak reduction

reduce-pe.agda

reduction/equality relation for strong reduction

normal-pe.agda

termination proof for strong reduction

This document was translated from L^AT_EX by H^EV^EA.