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.

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.