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.