2012/01/02 by Steven Obua, Obua, Steven
Computer Science · #Digital Libraries (cs.DL) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Mathematical Software (cs.MS) #cs.DL #cs.LO #cs.MS
paper · pdf · doi:10.48550/arxiv.1201.0540
arxiv created 2012/01/02 · arxiv updated 2012/01/04
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.