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",
}