Stages proposés dans l'équipe Marelle

(internship in the Marelle team)

• Efficient integer arithmetic in Coq.
• Translating terms in first-order logic to increase automation in Coq
• 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