Search

• < Previous
• 1
• Next >

Proof-Relevant Logical Relations for Name Generation

Pitts and Stark's $\nu$-calculus is a paradigmatic total language for studying the problem of contextual equivalence in higher-order languages with name generation. Models for the $\nu$-calculus that validate basic equivalences concerning names may be constructed using functor categories or nominal&nbsp;[&hellip;]