The high-level idea is that, LLVM IR gives us more control (over performance) than relying on the optimiser of C compilers. A novel way to establish the Cogent-LLVM refinement proof will also be explored.
Current Status
The code generation is currently being investigated as a student project.
Description
The high-level idea is that, LLVM IR gives us more control (over performance) than relying on the optimiser of C compilers. A novel way to establish the Cogent-LLVM refinement proof will also be explored.
Current Status
The code generation is currently being investigated as a student project.