Pilsner: a compositionally verified compiler for a higher-order imperative language
From MaRDI portal
Publication:2981953
DOI10.1145/2784731.2784764zbMath1360.68350MaRDI 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
transitivity; recursive types; abstract types; compositional compiler verification; higher-order state; parametric simulations
68N20: Theory of compilers and interpreters
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
The verified CakeML compiler backend, 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
Uses Software