Nominal LCF: A Language for Generic Proof
Programming Languages
2016-05-17 v2
Abstract
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. We contribute a new language to deal with the dynamic and interactive character of names in tactic scripts called Nominal LCF, and endow it with a denotational semantics in dI-domains. A large fragment of Nominal LCF has already been implemented and used to great effect in the new RedPRL proof assistant.
Keywords
Cite
@article{arxiv.1605.02142,
title = {Nominal LCF: A Language for Generic Proof},
author = {Jonathan Sterling},
journal= {arXiv preprint arXiv:1605.02142},
year = {2016}
}
Comments
Accepted to TFP 2016, the paper has been withdrawn by the author because he has found a serious flaw in the denotational semantics given in section 5