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

DOI10.1145/2784731.2784764zbMath1360.68350OpenAlexW2165594098MaRDI QIDQ2981953

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

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

transitivityrecursive typesabstract typescompositional compiler verificationhigher-order stateparametric simulations

Mathematics Subject Classification ID

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

Related Items (4)

Trace-Relating Compiler Correctness and Secure Compilation ⋮ Safe functional systems through integrity types and verified assembly ⋮ A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs ⋮ The verified CakeML compiler backend

Uses Software

• Coq
• Pilsner

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