A program logic for fresh name generation
Logic in Computer Science
2021-03-16 v2 Programming Languages
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.
Cite
@article{arxiv.2101.10720,
title = {A program logic for fresh name generation},
author = {Harold Pancho Eliott and Martin Berger},
journal= {arXiv preprint arXiv:2101.10720},
year = {2021}
}
Comments
15 core pages accepted for publication in FSEN 2021, +60 pages of proofs included in appendix