Stages proposés dans l'équipe Marelle

(internship in the Marelle team)

• Integrating the Metis automatic theorem prover into the Coq proof assistant
• Data-Mining and Refactoring for arithmetic in Coq
• Formalisation of linear algebra
• Formal proof of a theorem about biological models