State-dependent representation independence

DOI10.1145/1480881.1480925MaRDI QIDQ5261531zbMATHOpenAlexWikidataFDO

Authors Amal Ahmed, Derek Dreyer, 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

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

Recommendations

• A relational realizability model for higher-order stateful ADTs
• A relational modal logic for higher-order stateful ADTs
• Non-parametric parametricity
• Non-parametric parametricity
• scientific article; zbMATH DE number 3854400

Cited in

(38)

• Contextual approximation and higher-order procedures
• Complete trace models of state and control
• Non-parametric parametricity
• Noninterference in a predicative polymorphic calculus for access control
• Time bounds for general function pointers
• State dependent choice
• A language-independent proof system for full program equivalence
• scientific article; zbMATH DE number 3854400 (Why is no real title available?)
• Refactoring and representation independence for class hierarchies
• Relational cost analysis in a functional-imperative setting
• A Complete, Co-inductive Syntactic Theory of Sequential Control and State
• Holistic Specifications for Robust Programs
• A relational modal logic for higher-order stateful ADTs
• Algorithmic games for full ground references
• A bisimulation-like proof method for contextual properties in untyped \(\lambda \)-calculus with references and deallocation
• Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
• A relational realizability model for higher-order stateful ADTs
• A Complete Characterization of Observational Equivalence in Polymorphic λ-Calculus with General References
• New
• Logical relations for coherence of effect subtyping
• The category-theoretic solution of recursive metric-space equations
• Non-parametric parametricity
• Modal crash types for intermittent computing
• From bounded checking to verification of equivalence via symbolic up-to techniques
• A fragment of ML decidable by visibly pushdown automata
• Observational program calculi and the correctness of translations
• Signature restriction for polymorphic algebraic effects
• Algorithmic nominal game semantics
• Bifibrational functorial semantics of parametric polymorphism
• Transfinite step-indexing: decoupling concrete and logical steps
• Finite-state independence
• scientific article; zbMATH DE number 7407781 (Why is no real title available?)
• Parametric Polymorphism — Universally
• Automata-theoretic semantics of idealized Algol with passive expressions
• A Kripke logical relation for effect-based program transformations
• GADTs, functoriality, parametricity: pick two
• Program equivalence in a simple language with state
• Universal properties for universal types in bifibrational parametricity

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

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