2021/01/26 by Harold Pancho Eliott, Martin Berger, Eliott, Harold Pancho +1
Computer Science · #Logic, programming, and type systems #Software Engineering Research #Topic Modeling
paper · pdf · doi:10.48550/arxiv.2101.10720
We present a program logic for Pitts and Stark's ν-calculus, an extension of the call-by-value simply-typed λ-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.