Nominal LCF: A Language for Generic Proof

TL;DR

Nominal LCF introduces a new language with denotational semantics to handle dynamic hypothesis names in tactic scripts, improving proof management in interactive theorem proving environments.

Contribution

It presents Nominal LCF, a novel language for managing hypothesis names with a formal denotational semantics, addressing a key challenge in tactic language design.

Findings

Implemented a large fragment of Nominal LCF in RedPRL

Demonstrated effective handling of hypothesis names in proof scripts

Enhanced proof script flexibility and clarity

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.