Extracting and Optimizing Formally Verified Code for Systems Programming
MCQC is a compiler for extracting verified systems programs to low-level assembly, with no runtime or garbage collection requirements and an emphasis on performance. MCQC targets the Gallina functional language used in the Coq proof assistant. MCQC translates pure and recursive functions into C++17,...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Book |
| Language: | English |
| Published: |
Springer International Publishing
2020
|
| Online Access: | https://hdl.handle.net/1721.1/125251 |