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

DOI10.1017/S095679681200024XzbMath1252.68187OpenAlexW2101443478MaRDI QIDQ3165524

Derek R. Dreyer, Georg Neis, Lars Birkedal

Publication date: 29 October 2012

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s095679681200024x

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) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (10)

On the Versatility of Open Logical Relations ⋮ A Sound and Complete Bisimulation for Contextual Equivalence in $$\lambda $$ -Calculus with Call/cc ⋮ Parametric Polymorphism — Universally ⋮ Universal properties for universal types in bifibrational parametricity ⋮ Bifibrational functorial semantics of parametric polymorphism ⋮ Complete trace models of state and control ⋮ Transfinite Step-Indexing: Decoupling Concrete and Logical Steps ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item

Uses Software

• Haskell

Cites Work

• Functions with local state: regularity and undecidability
• The revised report on the syntactic theories of sequential control and state
• Classical logic, storage operators and second-order lambda-calculus
• Third-order Idealized Algol with iteration is decidable
• A bisimulation for type abstraction and recursion
• Logical Reasoning for Higher-Order Functions with Local State
• Short cut fusion is correct
• Equivalence in functional languages with effects

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