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