State-dependent representation independence

DOI10.1145/1480881.1480925zbMath1315.68080OpenAlexW2100559921WikidataQ60142689 ScholiaQ60142689MaRDI QIDQ5261531

Derek R. Dreyer, Amal Ahmed, Andreas Rossberg

Publication date: 3 July 2015

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

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.413.3977

zbMATH Keywords

abstract data typeslocal stateexistential typesrepresentation independencestep-indexed logical relations

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of programming languages (68N15) Abstract data types; algebraic specification (68Q65) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (28)

Automata-theoretic semantics of idealized Algol with passive expressions ⋮ Holistic Specifications for Robust Programs ⋮ A Kripke logical relation for effect-based program transformations ⋮ New ⋮ Time Bounds for General Function Pointers ⋮ A Complete, Co-inductive Syntactic Theory of Sequential Control and State ⋮ Algorithmic games for full ground references ⋮ The category-theoretic solution of recursive metric-space equations ⋮ Parametric Polymorphism — Universally ⋮ A bisimulation-like proof method for contextual properties in untyped \(\lambda \)-calculus with references and deallocation ⋮ Refactoring and representation independence for class hierarchies ⋮ A relational realizability model for higher-order stateful ADTs ⋮ Universal properties for universal types in bifibrational parametricity ⋮ Bifibrational functorial semantics of parametric polymorphism ⋮ Program equivalence in a simple language with state ⋮ Algorithmic Nominal Game Semantics ⋮ Complete trace models of state and control ⋮ A Fragment of ML Decidable by Visibly Pushdown Automata ⋮ A language-independent proof system for full program equivalence ⋮ Transfinite Step-Indexing: Decoupling Concrete and Logical Steps ⋮ Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types ⋮ Contextual Approximation and Higher-Order Procedures ⋮ Unnamed Item ⋮ A Complete Characterization of Observational Equivalence in Polymorphic λ-Calculus with General References ⋮ Unnamed Item ⋮ Noninterference in a predicative polymorphic calculus for access control ⋮ Observational program calculi and the correctness of translations ⋮ Relational cost analysis in a functional-imperative setting

This page was built for publication: State-dependent representation independence