31 citations · 52 across the 8 of their papers we have counts for
Showing 2010Show all
2 papers · 1 filter
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…