TY - GEN

T1 - Narrating formal proof (work in progress)

AU - Tankink, C.

AU - Geuvers, J.H.

AU - McKinna, J.

PY - 2012

Y1 - 2012

N2 - 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

AB - 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

U2 - 10.1016/j.entcs.2012.06.007

DO - 10.1016/j.entcs.2012.06.007

M3 - Conference contribution

T3 - Electronic Notes in Theoretical Computer Science

SP - 71

EP - 83

BT - Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers (UITP10, Edinburgh, UK, July 15, 2010)

A2 - Aspinall, D.

A2 - Sacerdoti Coen, C.

PB - ENTCS

T2 - conference; 9th International Workshop On User Interfaces for Theorem Provers; 2010-07-15; 2010-07-15

Y2 - 15 July 2010 through 15 July 2010

ER -