2 papers
cs.MS2012
Point-and-write --- Documenting Formal Mathematics by Reference
Carst Tankink, Christoph Lange, Josef Urban
This paper describes the design and implementation of mechanisms for light-weight inclusion of formal mathematics in informal mathematical writings, particularly in a Web-based set…
cs.LO2010
Proviola: A Tool for Proof Re-animation
Carst Tankink, Herman Geuvers, James McKinna +1
To improve on existing models of interaction with a proof assistant (PA), in particular for storage and replay of proofs, we in- troduce three related concepts, those of: a proof m…