A kripke logical relation between ML and assembly

DOI10.1145/1926385.1926402zbMath1284.68148MaRDI 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

biorthogonality; garbage collection; self-modifying code; step-indexed Kripke logical relations; compositional compiler correctness

Mathematics Subject Classification ID

68N20: Theory of compilers and interpreters

68N18: Functional programming and lambda calculus

03B70: Logic in computer science

68Q60: Specification and verification (program logics, model checking, etc.)

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

Unnamed Item, Trace-Relating Compiler Correctness and Secure Compilation, Pointers in Recursion: Exploring the Tropics, Correctness of compiling polymorphism to dynamic typing, Universal properties for universal types in bifibrational parametricity, Bifibrational functorial semantics of parametric polymorphism, 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, A language-independent proof system for full program equivalence, Fully abstract trace semantics for protected module architectures, Observational program calculi and the correctness of translations, Transfinite Step-Indexing: Decoupling Concrete and Logical Steps, A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs, Parametric Polymorphism — Universally