Pilsner
From MaRDI portal
Cited in
(17)- Safe functional systems through integrity types and verified assembly
- Pilsner: a compositionally verified compiler for a higher-order imperative language
- A verified compiler from Isabelle/HOL to CakeML
- Refinement through restraint: bringing down the cost of verification
- MoSeL
- CompCertTSO
- Vellvm
- Mezzo
- Flicker
- Kami
- Haskell Show Class
- IOzone
- CakeML_Codegen
- Nominal2
- The verified CakeML compiler backend
- Trace-relating compiler correctness and secure compilation
- A higher-order abstract syntax approach to verified transformations on functional programs
This page was built for software: Pilsner
