Biorthogonality, step-indexing and compiler correctness

DOI10.1145/1596550.1596567zbMath1302.68083OpenAlexW2104795876MaRDI QIDQ2936808

Chung-Kil Hur, Nick Benton

Publication date: 6 January 2015

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

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

zbMATH Keywords

biorthogonalitydenotational semanticsproof assistantscompiler verificationstep-indexing

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

A System-Level Game Semantics ⋮ Some Domain Theory and Denotational Semantics in Coq ⋮ Strongly typed term representations in Coq ⋮ A formally verified compiler back-end ⋮ 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 ⋮ Proving correctness of a compiler using step-indexed logical relations ⋮ 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 ⋮ Observational program calculi and the correctness of translations ⋮ Realizability models for a linear dependent PCF

Uses Software

• Coq
• VLISP