A First-Order Language for Expressing Aliasing and Type Properties of Logic Programs
Abstract elided by the publisher.
Related papers
- Expressing heap-shape contracts in linear logic GPCE 2006
- Beyond the elementary representations of program invariants over algebraic data types PLDI 2021
- On the Versatility of Open Logical Relations - Continuity, Automatic Differentiation, and a Containment Theorem ESOP 2020
- Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs POPL 2024
- Program Verification Based on Denotational Semantics POPL 1981
- RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code PLDI 2022
- Constraints: A Uniform Approach to Aliasing and Typing POPL 1985
- Reachability types: tracking aliasing and separation in higher-order functional programs OOPSLA 2021