Cooperative Repositories for Formal Proofs

We present a new framework for the online development of formalized mathematics. This framework allows wiki-style collaboration while providing users with a rendered and browsable version of their work. We describe a prototype based on Coq, its web interface as implemented by the second author, and a modified version of the MediaWiki code-base. We discuss open issues such as dependencies and repository consistency. We explain limitations of the current prototype and we give a perspective towards a more robust solution.

• Type: Conference
• Year: 2007
• Where: MKM
• Authors: Pierre Corbineau, Cezary Kaliszyk
• Keywords: Browsable Version, Current Prototype, MKM 2007, Wiki-style Collaboration