State-dependent representation independence

DOI10.1145/1480881.1480925MaRDI QIDQ5261531zbMATH OpenOpenAlexWikidataFDO

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 typesexistential typeslocal staterepresentation independencestep-indexed logical relations

Mathematics Subject Classification ID

Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) 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

(43)

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

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)