STAMP

The STAMP project-team studies the formal verification of algorithms and mathematical results using interactive proof tools like Coq/Rocq.  The favored application domain concerns formalized robotics.  Most notable contributions are related to the Coq/Rocq proof assistant, the Mathematical Components formally verified mathematics library, and the meta programming framework Elpi.