Narrating Formal Proof (Work in Progress)

Carst Tankink, Herman Geuvers, James McKinna

Research output: Contribution to journalArticle

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).].
Original languageEnglish
Pages (from-to)71-83
Number of pages13
JournalElectronic Notes in Theoretical Computer Science
Volume285
DOIs
Publication statusPublished - 19 Sep 2012

Fingerprint Dive into the research topics of 'Narrating Formal Proof (Work in Progress)'. Together they form a unique fingerprint.

Cite this