2012/01/02 by Obua, Steven
#Digital Libraries (cs.DL) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Mathematical Software (cs.MS)
paper · doi:10.48550/arxiv.1201.0540
ProofPeer strives to be a system for cloud-based interactive theorem proving. After illustrating why such a system is needed, the paper presents some of the design challenges that ProofPeer needs to meet to succeed. Contexts are presented as a solution to the problem of sharing proof state among the users of ProofPeer. Chronicles are introduced as a way to organize and version contexts.