Narrating Formal Proof (Work in Progress)

Carst Tankink; Herman Geuvers; James McKinna

doi:10.1016/j.entcs.2012.06.007

Narrating Formal Proof (Work in Progress)

Carst Tankink, Herman Geuvers, James McKinna

Research output: Contribution to journal › Article › peer-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).].

Original language	English
Pages (from-to)	71-83
Number of pages	13
Journal	Electronic Notes in Theoretical Computer Science
Volume	285
DOIs	https://doi.org/10.1016/j.entcs.2012.06.007
Publication status	Published - 19 Sept 2012

Access to Document

10.1016/j.entcs.2012.06.007Licence: CC BY-NC-ND

Cite this

@article{b7916be328d843a18b6f9b46cc54475f,

title = "Narrating Formal Proof (Work in Progress)",

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).].",

author = "Carst Tankink and Herman Geuvers and James McKinna",

year = "2012",

month = sep,

day = "19",

doi = "10.1016/j.entcs.2012.06.007",

language = "English",

volume = "285",

pages = "71--83",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

}

TY - JOUR

T1 - Narrating Formal Proof (Work in Progress)

AU - Tankink, Carst

AU - Geuvers, Herman

AU - McKinna, James

PY - 2012/9/19

Y1 - 2012/9/19

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).].

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).].

U2 - 10.1016/j.entcs.2012.06.007

DO - 10.1016/j.entcs.2012.06.007

M3 - Article

SN - 1571-0661

VL - 285

SP - 71

EP - 83

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

ER -

Narrating Formal Proof (Work in Progress)

Abstract

Access to Document

Fingerprint

Cite this