We have experimented with this first approach, using the course notes of Pierce et al. The dynamic quality of original movies, combined with the narrative of a literate proof script. These paragraphs are then used to display a marked up (or 'narrated') movie, that retainsġ571-0661/$ - see front matter © 2012 Elsevier B.V.
#CREATE FRAME TEXMACS MOVIE#
In this paper, we discuss our ongoing work in enriching the movie data structure with explanatory narrative, and the methods and tools we are developing to support such 'commentary' (which we think of as akin to multiple possible 'soundtracks' to a real movie).Ī first approximation is to emulate existing practice using the Coqdoc (available as part of the Coq distribution ) or JavaDoc style, whereby specially marked comments are extracted from an existing proof script to form the narrative. A movie is rendered as a webpage, that dynamically displays, without further interaction with the PA, the response to a given command when the reader hovers over it. In previous work, we presented the movie data structure that contains both a finished proof script and the PA responses to the commands in the script each response is linked to the command in a frame. However, the communication of proof texts to outsiders, such as mathematicians or students, has in our view not received the attention it deserves. Much research in user interfaces for Proof Assistants (PAs) has gone into facilitating the authoring of (formal) proof documents. Keywords: Coursebooks, Proof Assistants, Proof Communication In this setting, we have studied extracting commentary from an online text by Pierce et al.
#CREATE FRAME TEXMACS HOW TO#
We have now considered the problem of how to augment this movie data structure to support commentary on formal proof development.
Radboud University Institute for Computing and Information Science Nijmegen, The Netherlandsīuilding on existing work in proxying interaction with proof assistants, we have previously developed a proof movie. Narrating Formal Proof (Work in Progress)Ĭarst Tankink Herman Geuvers James McKinna
Available online at SciVerse ScienceDirectĮlectronic Notes in Theoretical Computer Science 285 (2012) 71-83
0 kommentar(er)
