17 citations · 39 across the 7 of their papers we have counts for
7 papers
Statman's Hierarchy Theorem
Bram Westerbaan, Bas Westerbaan, Rutger Kuyper +3
In the Simply Typed -calculus Statman investigates the reducibility relation between types: for , types freely generated using an…
Asynchronous processing of Coq documents: from the kernel up to the user interface
Bruno Barras, Carst Tankink, Enrico Tassi
The work described in this paper improves the reactivity of the Coq system by completely redesigning the way it processes a formal document. By subdividing such work into independe…
PIDE for Asynchronous Interaction with Coq
Carst Tankink
This paper describes the initial progress towards integrating the Coq proof assistant with the PIDE architecture initially developed for Isabelle. The architecture is aimed at asyn…
Proof in Context -- Web Editing with Rich, Modeless Contextual Feedback
Carst Tankink
The Agora system is a prototypical Wiki for formal mathematics: a web-based system for collaborating on formal mathematics, intended to support informal documentation of formal dev…
Formal Mathematics on Display: A Wiki for Flyspeck
Carst Tankink, Cezary Kaliszyk, Josef Urban +1
The Agora system is a prototype "Wiki for Formal Mathematics", with an aim to support developing and documenting large formalizations of mathematics in a proof assistant. The funct…
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…
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…