Jonathan Sterling

Nominal LCF: A Language for Generic Proof

2016 · arXiv (Cornell University)

The syntax and semantics of user-supplied hypothesis names in tactic languages is a thorny problem, because the binding structure of a proof is a function of the goal at which a tactic script is executed. …