A verified compiler for an impure functional language

DOI10.1145/1706299.1706312MaRDI QIDQ5255065zbMATH OpenOpenAlexWikidataFDO

Authors Adam Chlipala

Publication date 11 June 2015

Published in Proceedings of the 37th 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/1706299.1706312

zbMATH Keywords

compiler verificationinteractive proof assistants

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 2079040
• A linear first-order functional intermediate language for verified compilers
• A formally verified compiler back-end
• Pilsner: a compositionally verified compiler for a higher-order imperative language
• The verified CakeML compiler backend

Cited in

(14)

• Proving correctness of a compiler using step-indexed logical relations
• Safe functional systems through integrity types and verified assembly
• Observational program calculi and the correctness of translations
• Biorthogonality, step-indexing and compiler correctness
• Calculating certified compilers for non-deterministic languages
• A linear first-order functional intermediate language for verified compilers
• Pilsner: a compositionally verified compiler for a higher-order imperative language
• Programming inductive proofs. A new approach based on contextual types
• A verified runtime for a verified theorem prover
• scientific article; zbMATH DE number 2079040 (Why is no real title available?)
• A provably correct compilation of functional languages into scripting languages
• The verified CakeML compiler backend
• The correctness of a code generator for a functional language
• A verified framework for higher-order uncurrying optimizations

Describes a project that uses

Uses Software

• Coq

This page was built for publication: A verified compiler for an impure functional language

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5255065)