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

DOI10.1145/1863543.1863566zbMath1323.68203OpenAlexW2153128836MaRDI 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

biorthogonalitystate transition systemsobservational equivalencelocal stateexceptionshigher-order statefirst-class continuationsstep-indexed Kripke logical relations

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) 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 (10)

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

Uses Software

• Haskell

This page was built for publication: The impact of higher-order state and control effects on local relational reasoning