Pilsner: a compositionally verified compiler for a higher-order imperative language

DOI10.1145/2784731.2784764MaRDI QIDQ2981953zbMATH OpenOpenAlexWikidataFDO

Authors Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig A. McLaughlin, Derek Dreyer, Viktor Vafeiadis

Publication date 10 May 2017

Published in Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)

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

zbMATH Keywords

abstract typescompositional compiler verificationhigher-order stateparametric simulationsrecursive typestransitivity

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A verified compiler for an impure functional language
• A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler
• scientific article; zbMATH DE number 2079040
• A compositional approach to CTL^* verification
• A linear first-order functional intermediate language for verified compilers
• Toward compiler implementation correctness proofs

Cited in

(10)

• Safe functional systems through integrity types and verified assembly
• A higher-order abstract syntax approach to verified transformations on functional programs
• Lightweight verification of separate compilation
• A linear first-order functional intermediate language for verified compilers
• scientific article; zbMATH DE number 2081101 (Why is no real title available?)
• The verified CakeML compiler backend
• Trace-relating compiler correctness and secure compilation
• A verified compiler for an impure functional language
• Verifying peephole rewriting in SSA compiler IRs
• A logical approach to type soundness

Describes a project that uses

Uses Software

• Pilsner
• Coq

This page was built for publication: Pilsner: a compositionally verified compiler for a higher-order imperative language

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