A kripke logical relation for effect-based program transformations

DOI10.1145/2034773.2034831zbMath1323.68230OpenAlexW4244977193MaRDI QIDQ5176994

Jacob Thamsborg, Lars Birkedal

Publication date: 5 March 2015

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

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

zbMATH Keywords

program transformationsultrametric spacestype and effect systemKripke logical relationstep-indexed modeldangling pointerseffect masking

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (4)

Nominal lambda calculus: an internal language for FM-Cartesian closed categories ⋮ Automata-theoretic semantics of idealized Algol with passive expressions ⋮ A Kripke logical relation for effect-based program transformations ⋮ StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities

This page was built for publication: A kripke logical relation for effect-based program transformations