Narrating formal proof (work in progress)

C. Tankink, J.H. Geuvers, J. McKinna

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

Building on existing work in proxying interaction with proof assistants, we have previously developed a proof movie. We have now considered the problem of how to augment this movie data structure to support commentary on formal proof development. In this setting, we have studied extracting commentary from an online text by Pierce et al. [Pierce, B. C., C. Casinghino and M. Greenberg, Software foundations, Course notes, online at http://www.cis.upenn.edu/~bcpierce/sf/ (2010).]. Keywords: Coursebooks; Proof Assistants; Proof Communication
Original languageEnglish
Title of host publicationProceedings of the 9th International Workshop On User Interfaces for Theorem Provers (UITP10, Edinburgh, UK, July 15, 2010)
EditorsD. Aspinall, C. Sacerdoti Coen
PublisherENTCS
Pages71-83
DOIs
Publication statusPublished - 2012
Eventconference; 9th International Workshop On User Interfaces for Theorem Provers; 2010-07-15; 2010-07-15 -
Duration: 15 Jul 201015 Jul 2010

Publication series

NameElectronic Notes in Theoretical Computer Science
Volume285
ISSN (Print)1571-0061

Conference

Conferenceconference; 9th International Workshop On User Interfaces for Theorem Provers; 2010-07-15; 2010-07-15
Period15/07/1015/07/10
Other9th International Workshop On User Interfaces for Theorem Provers

Fingerprint

Dive into the research topics of 'Narrating formal proof (work in progress)'. Together they form a unique fingerprint.

Cite this