A Kripke logical relation between ML and assembly
DOI10.1145/1926385.1926402zbMATH Open1284.68148OpenAlexW4252501555MaRDI QIDQ5408538FDOQ5408538
Authors: Chung-Kil Hur, Derek Dreyer 
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
Recommendations
- Biorthogonality, step-indexing and compiler correctness
- Proving correctness of a compiler using step-indexed logical relations
- A Kripke logical relation for effect-based program transformations
- A Kripke logical relation for effect-based program transformations
- Correctness of procedure representations in higher-order assembly language
biorthogonalitygarbage collectionself-modifying codestep-indexed Kripke logical relationscompositional compiler correctness
Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)
Cited In (20)
- Correctness of compiling polymorphism to dynamic typing
- Proving correctness of a compiler using step-indexed logical relations
- Transfinite step-indexing: decoupling concrete and logical steps
- Fully abstract trace semantics for protected module architectures
- Universal properties for universal types in bifibrational parametricity
- Observational program calculi and the correctness of translations
- Biorthogonality, step-indexing and compiler correctness
- 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
- Bifibrational functorial semantics of parametric polymorphism
- Title not available (Why is that?)
- Parametric Polymorphism — Universally
- Logical predicates in higher-order mathematical operational semantics
- A Kripke logical relation for effect-based program transformations
- A language-independent proof system for full program equivalence
- Trace-relating compiler correctness and secure compilation
- GADTs, functoriality, parametricity: pick two
- Correctness of procedure representations in higher-order assembly language
- A higher-order abstract syntax approach to verified transformations on functional programs
- Pointers in Recursion: Exploring the Tropics
This page was built for publication: A Kripke logical relation between ML and assembly
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5408538)
