A verified framework for higher-order uncurrying optimizations

The Coq development

This page contains the Coq development accompanying the following article:

Zaynah Dargaye and Xaver Leroy, A verified framework for higher-order uncurrying optimizations, submitted, March 2009.

Pretty-printed Coq sources:

Uncurry The general framework and its proof of correctness (sections 2 and 4 of the paper)
Firstorder Application to first-order uncurrying (section 5.1)
TranslValid Translation validation (section 5.2)
Coqlib Useful Coq definitions and lemmas
ErrorMonad The error monad

A .tgz archive of the Coq sources. Require Coq version 8.1 or later.

Copyright 2008, 2009 Institut National de Recherche en Informatique et Automatique (INRIA). These files are distributed under the terms of the GNU Public License version 2.