A program logic for fresh name generation
From MaRDI portal
Publication:2145263
DOI10.1007/978-3-030-89247-0_6zbMATH Open1496.68103arXiv2101.10720OpenAlexW3210061875MaRDI QIDQ2145263FDOQ2145263
Martin Berger, Harold Pancho Eliott
Publication date: 17 June 2022
Abstract: We present a program logic for Pitts and Stark's {
u}-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.
Full work available at URL: https://arxiv.org/abs/2101.10720
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70)
Cites Work
- Nominal logic, a first order theory of names and binding
- Nominal sets. Names and symmetry in computer science
- The impact of higher-order state and control effects on local relational reasoning
- A new approach to abstract syntax with variable binding
- A calculus of mobile processes. II
- Types and programing languages
- Logical Reasoning for Higher-Order Functions with Local State
- Title not available (Why is that?)
- Automated Deduction – CADE-20
- Elementary structures in process theory (1): Sets with renaming
- Program Logics for Homogeneous Generative Run-Time Meta-Programming
Cited In (1)
Uses Software
This page was built for publication: A program logic for fresh name generation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2145263)
