4 citations · 8 across the 3 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
cs.LO2012★ 4 cited
The lambda-mu-T-calculus
Herman Geuvers, Robbert Krebbers, James McKinna
Calculi with control operators have been studied as extensions of simple type theory. Real programming languages contain datatypes, so to really understand control operators, one s…
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…