The impact of higher-order state and control effects on local relational reasoning

DOI10.1145/1863543.1863566zbMath1323.68203MaRDI QIDQ5176935

Georg Neis, Derek R. Dreyer, Lars Birkedal

Publication date: 5 March 2015

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

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

zbMATH Keywords

biorthogonality; state transition systems; observational equivalence; local state; exceptions; higher-order state; first-class continuations; step-indexed Kripke logical relations

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

68Q55: Semantics in the theory of computing

68Q60: Specification and verification (program logics, model checking, etc.)

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

From Applicative to Environmental Bisimulation, Automata-theoretic semantics of idealized Algol with passive expressions, A relational realizability model for higher-order stateful ADTs, Program equivalence in a simple language with state, Algorithmic games for full ground references, Proving correctness of a compiler using step-indexed logical relations, A program logic for fresh name generation, Algorithmic probabilistic game semantics. Playing games with automata, A Kripke logical relation for effect-based program transformations, Algorithmic Nominal Game Semantics

Uses Software

• Haskell