Details of Grant 

EPSRC Reference:	EP/L011794/1
Title:	ProofPeer: Collaborative Theorem Proving
Principal Investigator:	Fleuriot, Dr J
Other Investigators:	Aspinall, Professor D
Researcher Co-Investigators:	Dr S Obua
Project Partners:
Department:	Sch of Informatics
Organisation:	University of Edinburgh
Scheme:	Standard Research
Starts:	01 April 2014	Ends:	31 March 2017	Value (£):	522,808
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:	Panel Date Panel Name Outcome 24 Oct 2013 EPSRC ICT Responsive Mode - Oct 2013 Announced
Summary on Grant Application Form
In today's computerised and scientific era, making our claims indefeasible is more critical and more relevant than ever. We need to make indefeasible claims about the stability of mission critical hardware and software components, e.g. about technology used in medicine where mistakes can be deadly, or about the security of computer systems in times where computer viruses are used as weapons of warfare. In response to the challenge of making indefeasible claims, the fields of automated and interactive theorem proving have emerged. Automated theorem proving (ATP) is the mechanical checking of computerised proofs by mostly black box software components. Interactive theorem proving (ITP) builds on this by allowing human insight to guide and coordinate ATP systems in almost arbitrary ways. Interactive theorem proving has had noteworthy successes like the mechanisation of the proof of the four-colour theorem, or the proof of the correctness of the seL4 operating system microkernel. These two examples show that verification problems in very different domains like pure mathematics and system level software can be successfully solved using the same technology, interactive theorem proving. We believe that the time has come to reach even further and to be even more ambitious about the size of verification projects we are trying to tackle. But to be able to do so, we need a paradigm shift. The Linux operating system kernel consists of fifteen million lines of C program source code which has been contributed by over 1300 developers and over 200 companies. The verification of this kernel is completely out of reach for current ITP technology by several orders of magnitude. While we manage to develop software at scale, it is as yet unknown how to do verification at scale. We therefore propose to expand the capabilities of ITP by creating collaborative theorem proving (CTP). We shall take the lessons and technologies of interactive theorem proving and integrate the lessons and technologies of the social web, in particular: 1) commons-based peer production and crowd-sourcing, 2) reputation systems, and 3) recommender systems. Sites like Wikipedia, Stack Overflow and Math Overflow have proven that these three components of the social web can result in unprecedented collaborative productivity. The focus of our research will be how to harness this productivity for the purpose of interactive theorem proving, establishing collaborative theorem proving as the social machine of ITP. To this end, we will grow a online community called ProofPeer, which will be centrally hosted at http://proofpeer.net. After an initial phase of research and implementation, anyone will be able to become a proof peer and participate in this experiment of collaborative theorem proving.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.ed.ac.uk