Overview

The STAMP projet-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.

Research directions

• Type Theory
• Proof Theory
• Formal Verification
• Cryptography
• Robotics
• Generation and Automatic Transformation of Formal Proofs
• Generation and Automatic Transformation of Safe Programs