A kripke logical relation between ML and assembly

DOI10.1145/1926385.1926402zbMath1284.68148OpenAlexW4252501555MaRDI QIDQ5408538

Derek R. Dreyer, Chung-Kil Hur

Publication date: 10 April 2014

Published in: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

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

zbMATH Keywords

biorthogonalitygarbage collectionself-modifying codestep-indexed Kripke logical relationscompositional compiler correctness

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (14)

Trace-Relating Compiler Correctness and Secure Compilation ⋮ Parametric Polymorphism — Universally ⋮ A type-directed, dictionary-passing translation of method overloading and structural subtyping in Featherweight Generic Go ⋮ Semantic preservation for a type directed translation scheme of Featherweight Go ⋮ Correctness of compiling polymorphism to dynamic typing ⋮ Universal properties for universal types in bifibrational parametricity ⋮ Bifibrational functorial semantics of parametric polymorphism ⋮ A language-independent proof system for full program equivalence ⋮ Fully abstract trace semantics for protected module architectures ⋮ Transfinite Step-Indexing: Decoupling Concrete and Logical Steps ⋮ A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs ⋮ Pointers in Recursion: Exploring the Tropics ⋮ Unnamed Item ⋮ Observational program calculi and the correctness of translations

This page was built for publication: A kripke logical relation between ML and assembly