verified-compiler

Here are 3 public repositories matching this topic...

sigurdschneider / lvc

LVC verified compiler

compiler coq verification coq-formalization register-allocation compiler-design verified-compiler lvc lvc-compiler register-assignment spilling constant-propagation ssa-construction

Updated Nov 1, 2018
Coq

querycert / qcert

Star

Compilation and Verification of Data-Centric Languages

sql compiler functional-programming verification query-engine query-language verified-compiler coq-proof-assistant

Updated Jul 17, 2024
Coq

Research language whose affine/QTT core is proved sound twice — Coq and Idris2, axiom-free and CI-gated — with the verified usage-checker ported into the Rust compiler. Nested Solo ⊂ Duet ⊂ Ensemble dialects, session-typed concurrency, echo types for loss that isn't erasure. Early alpha.

session-types proof-engineering verified-compiler linear-types type-systems programming-language-design affine-types mechanized-metatheory quantitative-type-theory

Updated Aug 24, 2026
Rust

Improve this page

Add a description, image, and links to the verified-compiler topic page so that developers can more easily learn about it.

Curate this topic

Add this topic to your repo

To associate your repository with the verified-compiler topic, visit your repo's landing page and select "manage topics."

Learn more

Navigation Menu