Cooperative Repositories for Formal Proofs

DOI10.1007/978-3-540-73086-6_19MaRDI QIDQ5428272zbMATH OpenOpenAlexWikidataFDO

Authors Pierre Corbineau, Cezary Kaliszyk

Publication date 28 November 2007

Published in Towards Mechanized Mathematical Assistants (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73086-6_19

Mathematics Subject Classification ID

Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35)

Recommendations

• scientific article; zbMATH DE number 1951637
• scientific article; zbMATH DE number 1552521
• Re-imagining the Isabelle archive of formal proofs
• Mining the Archive of Formal Proofs
• Toward sharing libraries of mathematics between theorem provers
• Towards a formally verified proof assistant
• Coherence for sharing proof-nets
• Coherence for sharing proof nets
• scientific article; zbMATH DE number 1301751
• Collaborative Interactive Theorem Proving with Clide

Cited in

(11)

• Proof assistants: history, ideas and future
• Aligning concepts across proof assistant libraries
• Formal mathematics on display: a wiki for Flyspeck
• Point-and-write -- documenting formal mathematics by reference
• A Declarative Language for the Coq Proof Assistant
• A Wiki for Mizar: motivation, considerations, and initial prototype
• scientific article; zbMATH DE number 1951636 (Why is no real title available?)
• Large formal wikis: issues and solutions
• Communicating formal proofs: the case of Flyspeck
• Towards Knowledge Management for HOL Light
• Exploring formal math on the blockchain: an explorer for Proofgold

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Cooperative Repositories for Formal Proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5428272)