Proof-Relevant Logical Relations for Name Generation

Pitts and Stark's $\nu$-calculus is a paradigmatic total language forstudying the problem of contextual equivalence in higher-order languages withname generation. Models for the $\nu$-calculus that validate basic equivalencesconcerning names may be constructed using functor categories or nominal sets,with a dynamic allocation monad used to model computations that may allocatefresh names. If recursion is added to the language and one attempts to adaptthe models from (nominal) sets to (nominal) domains, however, the direct-styleconstruction of the allocation monad no longer works. This issue has previouslybeen addressed by using a monad that combines dynamic allocation withcontinuations, at some cost to abstraction. This paper presents a direct-style model of a $\nu$-calculus-like languagewith recursion using the novel framework of proof-relevant logical relations,in which logical relations also contain objects (or proofs) demonstrating theequivalence of (the semantic counterparts of) programs. Apart from providing afresh solution to an old problem, this work provides an accessible setting inwhich to introduce the use of proof-relevant logical relations, free of theadditional complexities associated with their use for more sophisticatedlanguages