A theory of indirection via approximation

DOI10.1145/1706299.1706322zbMath1312.68060OpenAlexW2145849916MaRDI QIDQ5255071

Andrew W. Appel, Aquinas Hobor, Robert Dockins

Publication date: 11 June 2015

Published in: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

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

zbMATH Keywords

step-indexed modelsindirection theory

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (7)

Bringing Order to the Separation Logic Jungle ⋮ Time Bounds for General Function Pointers ⋮ VST-Floyd: a separation logic tool to verify correctness of C programs ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic ⋮ Verified Software Toolchain ⋮ Barriers in Concurrent Separation Logic ⋮ Transfinite Step-Indexing: Decoupling Concrete and Logical Steps

Uses Software

• Coq

This page was built for publication: A theory of indirection via approximation