ProofScript: Proof Scripting for the Masses

Steven Obua, Phil Scott, Jacques Fleuriot

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

The goal of the ProofPeer project is to make collaborative theorem proving a reality. An important part of our plan to make this happen is ProofScript, a language designed to be the main user interface of ProofPeer. Of foremost importance in the design of ProofScript is its fit within a collaborative theorem proving environment. By this we mean that it needs to fit into an environment where peers who are not necessarily part of the current theorem proving and programming language communities work independently from but collaboratively with each other to produce formal definitions and proofs. All aspects of ProofScript are shaped by this design principle. In this paper we will discuss ProofScript’s most important aspect of being an integrated language both for interactive proof and for proof scripting.
Original languageEnglish
Title of host publicationTheoretical Aspects of Computing - ICTAC 2016
Subtitle of host publication13th International Colloquium, Taipei, Taiwan, ROC, October 24–31, 2016, Proceedings
PublisherSpringer International Publishing
Number of pages16
ISBN (Electronic)978-3-319-46750-4
ISBN (Print)978-3-319-46749-8
Publication statusPublished - 22 Sept 2016
Event13th International Colloquium on Theoretical Aspects of Computing - Taipei, Taiwan, Province of China
Duration: 24 Oct 201630 Oct 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
ISSN (Print)0302-9743


Conference13th International Colloquium on Theoretical Aspects of Computing
Abbreviated titleICTAC 2016
Country/TerritoryTaiwan, Province of China
Internet address


Dive into the research topics of 'ProofScript: Proof Scripting for the Masses'. Together they form a unique fingerprint.

Cite this