A compilation algorithm for parallel moves

The Coq development

This page contains the Coq development accompanying the following article:

Laurence Rideau, Bernard Paul Serpette and Xavier Leroy, Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves, 2007. Accepted for publication in Journal of Automated Reasoning.

• Pretty-printed Coq sources, for online viewing:
  • Parmov (the algorithm and its correctness proof)
  • Coqlib (auxiliary Coq definitions and lemmas)
• Raw Coq sources (require Coq version 8.1 or later).

Copyright 2005, 2006, 2007 Institut National de Recherche en Informatique et Automatique (INRIA). The Coq files are distributed under the terms of the GNU Public License version 2.