A program logic for fresh name generation

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.