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 language | English |
|---|---|
| Title of host publication | Theoretical Aspects of Computing - ICTAC 2016 |
| Subtitle of host publication | 13th International Colloquium, Taipei, Taiwan, ROC, October 24–31, 2016, Proceedings |
| Publisher | Springer |
| Pages | 333-348 |
| Number of pages | 16 |
| ISBN (Electronic) | 978-3-319-46750-4 |
| ISBN (Print) | 978-3-319-46749-8 |
| DOIs | |
| Publication status | Published - 22 Sept 2016 |
| Event | 13th International Colloquium on Theoretical Aspects of Computing - Taipei, Taiwan, Province of China Duration: 24 Oct 2016 → 30 Oct 2016 http://cc.ee.ntu.edu.tw/~ictac2016/ |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer International Publishing |
| Volume | 9965 |
| ISSN (Print) | 0302-9743 |
Conference
| Conference | 13th International Colloquium on Theoretical Aspects of Computing |
|---|---|
| Abbreviated title | ICTAC 2016 |
| Country/Territory | Taiwan, Province of China |
| City | Taipei |
| Period | 24/10/16 → 30/10/16 |
| Internet address |