Start Over

Narrating Formal Proof (Work in Progress)

Authors :: Tankink, C.
Geuvers, J.H.
McKinna, J.
Aspinall, D.
Sacerdoti Coen, C.
Aspinall, D.
Formal System Analysis
Source :: Electronic Notes in Theoretical Computer Science, 285, pp. 71-83, Tankink, C, Geuvers, H & McKinna, J 2012, ' Narrating Formal Proof (Work in Progress) ', Electronic Notes in Theoretical Computer Science, vol. 285, pp. 71-83 . https://doi.org/10.1016/j.entcs.2012.06.007, Aspinall, D. (ed.), Proceedings of the UITP'10, pp. 1-14, Aspinall, D. (ed.), Proceedings of the UITP'10, 1-14. [S.l : s.n], STARTPAGE=1;ENDPAGE=14;TITLE=Aspinall, D. (ed.), Proceedings of the UITP'10, Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers (UITP10, Edinburgh, UK, July 15, 2010), 71-83, STARTPAGE=71;ENDPAGE=83;TITLE=Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers (UITP10, Edinburgh, UK, July 15, 2010), Electronic Notes in Theoretical Computer Science, 285, 71-83
Publication Year :: 2012
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