A Kripke logical relation between ML and assembly
From MaRDI portal
biorthogonalitycompositional compiler correctnessgarbage collectionself-modifying codestep-indexed Kripke logical relations
Logic in computer science (03B70) Functional programming and lambda calculus (68N18) 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)
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
Cited in
(24)- Proving correctness of a compiler using step-indexed logical relations
- 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
- Biorthogonality, step-indexing and compiler correctness
- Parametric Polymorphism — Universally
- Trace-relating compiler correctness and secure compilation
- Pointers in Recursion: Exploring the Tropics
- A language-independent proof system for full program equivalence
- scientific article; zbMATH DE number 7407781 (Why is no real title available?)
- A Kripke logical relation for effect-based program transformations
- 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
- Correctness of procedure representations in higher-order assembly language
- Logical predicates in higher-order mathematical operational semantics
- GADTs, functoriality, parametricity: pick two
- Bialgebraic reasoning on higher-order program equivalence
- A logical approach to type soundness
- GADTs are not (even partial) functors
- On the semantic expressiveness of iso- and equi-recursive types
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)
