21 citations · 116 across the 21 of their papers we have counts for
Showing 2010 · cs.LOShow all
2 papers · 2 filters
cs.LO2010★ 8 cited
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…
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…