Abstract
We present a proof of the optimality of lambda-mix, a partial
evaluator for the untyped lambda calculus originally defined in 1989
by Carsten K. Gomard in his master's thesis. To the best of our
knowledge, this is the first proof of the optimality of a partial
evaluator, and we have mechanized the proof within Isabelle/HOL, the
typed higher order logic instance of the generic proof system
Isabelle. We present both a `normal' paper proof and the mechanized
proof, and report on our experiences with proving semantic properties
of a concrete program, rather than program transformations.
Files
BibTeX Entry
@mastersthesis
{
skalberg:opt-lambdamix,
author = "Sebastian C[hristian] Skalberg",
title = "Mechanical Proof of the Optimality of a Partial Evaluator",
school = "Department of Computer Science, University of Copenhagen",
year = "1999",
month = feb,
url = "http://www.mangust.dk/skalberg/msc/",
postscript = "http://www.mangust.dk/skalberg/msc/skalberg-msc.ps",
dvi = "http://www.mangust.dk/skalberg/msc/skalberg-msc.dvi",
}