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

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 LATEX by HEVEA.