A logical analysis of aliasing in imperative higher-order functions

DOI10.1145/1086365.1086401MaRDI QIDQ2936791zbMATH OpenOpenAlexFDO

Authors Martin Berger, Kohei Honda, Nobuko Yoshida

Publication date 6 January 2015

Published in Proceedings of the tenth ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1086365.1086401

zbMATH Keywords

\(\pi\)-calculusaliasingfunctional programmingHoare-logicsmodalitiespointerstyping

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A logical analysis of aliasing in imperative higher-order functions
• Aliasing Control in an Imperative Pure Calculus
• A formally-verified alias analysis
• scientific article; zbMATH DE number 1761902
• scientific article; zbMATH DE number 4178742
• An observationally complete program logic for imperative higher-order functions
• scientific article; zbMATH DE number 1948387
• Transformational derivation of an improved alias analysis algorithm
• Alias calculus for a simple imperative language with decidable pointer arithmetic
• Static Analysis

Cited in

(7)

• Laws of programming for references
• Aliasing Control in an Imperative Pure Calculus
• An observationally complete program logic for imperative higher-order functions
• Type-based security for mobile computing integrity, secrecy and liveness
• A logical analysis of aliasing in imperative higher-order functions
• Compiler Construction
• Transformational derivation of an improved alias analysis algorithm

This page was built for publication: A logical analysis of aliasing in imperative higher-order functions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2936791)