STAMP

The STAMP project-team studies the formal verification of algorithms and mathematical results using interactive proof tools like Coq or EasyCrypt.  The favored application domains concern cryptography and formalized robotics.  Most notable contributions are related to the Coq proof assistant, the EasyCrypt proof tool, and the Mathematical Components formally verified mathematics library.