The impact of higher-order state and control effects on local relational reasoning
From MaRDI portal
Publication:3165524
DOI10.1017/S095679681200024XzbMath1252.68187MaRDI 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
68N18: Functional programming and lambda calculus
68Q55: Semantics in the theory of computing
68Q60: Specification and verification (program logics, model checking, etc.)
68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Unnamed Item, Unnamed Item, On the Versatility of Open Logical Relations, Unnamed Item, 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, Parametric Polymorphism — Universally, A Sound and Complete Bisimulation for Contextual Equivalence in $$\lambda $$ -Calculus with Call/cc
Uses Software
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
