21 citations · 116 across the 21 of their papers we have counts for
3 papers · 1 filter
Pure Type Systems without Explicit Contexts
Herman Geuvers, Robbert Krebbers, James McKinna +1
We present an approach to type theory in which the typing judgments do not have explicit contexts. Instead of judgments of shape "Gamma |- A : B", our systems just have judgments o…
A Wiki for Mizar: Motivation, Considerations, and Initial Prototype
Josef Urban, Jesse Alama, Piotr Rudnicki +1
Formal mathematics has so far not taken full advantage of ideas from collaborative tools such as wikis and distributed version control systems (DVCS). We argue that the field could…
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…