A program logic for fresh name generation
From MaRDI portal
Publication:2145263
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.
Recommendations
Cites work
- scientific article; zbMATH DE number 4114587 (Why is no real title available?)
- A calculus of mobile processes. II
- A new approach to abstract syntax with variable binding
- Automated Deduction – CADE-20
- Elementary structures in process theory (1): Sets with renaming
- Logical Reasoning for Higher-Order Functions with Local State
- Nominal logic, a first order theory of names and binding
- Nominal sets. Names and symmetry in computer science
- Program logics for homogeneous generative run-time meta-programming
- The impact of higher-order state and control effects on local relational reasoning
- Types and programing languages
Cited in
(2)
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)
