A program logic for fresh name generation
Harold Pancho Eliott, Martin Berger

TL;DR
This paper introduces a program logic tailored for Pitts and Stark's b5-calculus, enabling formal reasoning about fresh name generation and equality, with applications to complex case analysis.
Contribution
It develops a novel logic incorporating second-order quantification over type contexts to handle fresh name generation in a call-by-value setting.
Findings
Logic effectively captures subtle observable properties of fresh names.
Enables reasoning about complex name generation scenarios.
Demonstrates applicability through difficult case studies.
Abstract
We present a program logic for Pitts and Stark's {\nu}-calculus, an extension of the call-by-value simply-typed {\lambda}-calculus with a mechanism for the generation of fresh names. Names can be compared for (in)-equality, producing programs with subtle observable properties. Hidden names produced by interactions between generation and abstraction are captured logically with a second-order quantifier over type contexts. We illustrate usage of the logic through reasoning about well-known difficult cases from the literature.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Software Engineering Research · Topic Modeling
