qcert
Compiler framework
A framework for developing and verifying domain-specific languages with a focus on compiler correctness and verification.
Compilation and Verification of Data-Centric Languages
56 stars
6 watching
9 forks
Language: Coq
last commit: 7 months ago
Linked from 1 awesome list
compilercoq-proof-assistantfunctional-programmingquery-enginequery-languagesqlverificationverified-compiler
Related projects:
| Repository | Description | Stars |
|---|---|---|
 certicoq/certicoq | A compiler for a subset of the C language that can be compiled with any standard C compiler, used in formal verification and proof assistance. | 137 |
 calyxir/calyx | An intermediate language and infrastructure for building compilers that generate custom hardware accelerators. | 503 |
 absint/compcert | A formally verified compiler for a subset of C that generates code for multiple architectures. | 1,901 |
 coq-community/chapar | A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant | 32 |
 qt/qtdeclarative | A comprehensive collection of libraries and modules for building user interfaces and dynamic applications using Qt's declarative language. | 231 |
 reynir/brainfuck | Formalizing Brainfuck in Coq to prove its properties and verify a compiler for simple arithmetic expressions. | 26 |
 qutech-delft/openql | A portable quantum programming framework for compiling and optimizing quantum code on various target platforms. | 101 |
| coq-community/coq-ext-lib | A collection of reusable Coq definitions and theorems for building software development tools | 129 |
| coq-community/fav-ssr | A comprehensive library of verified data structures and algorithms in Coq | 45 |
| coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
 cyq1162/cyqdata | A high-performance and powerful ORM (Object-Relational Mapping) framework for .NET that supports various databases. | 685 |
 pa-ba/calc-comp | Formalizations of compiler design and virtual machine calculations in Coq | 30 |
 dboulytchev/minikanren-coq | A certified semantics for relational programming language specification, providing verified implementations of syntax and semantics for miniKanren languages | 26 |
 xavierleroy/cdf-sem-meca | This project provides a development environment and software tools for formalizing the semantics of programming languages in the Coq proof assistant. | 21 |
| xavierleroy/cdf-mech-sem | Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |