uwplse / Crimp
Certified Relational to Imperative
Labels
Projects that are alternatives of or similar to Crimp
Coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Stars: ✭ 3,566 (+71220%)
Mutual labels: coq
Practical Fm
A gently curated list of companies using verification formal methods in industry
Stars: ✭ 272 (+5340%)
Mutual labels: coq
Category Theory
An axiom-free formalization of category theory in Coq for personal study and practical work
Stars: ✭ 562 (+11140%)
Mutual labels: coq
topology
General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
Stars: ✭ 36 (+620%)
Mutual labels: coq
Unimath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Stars: ✭ 680 (+13500%)
Mutual labels: coq
Verdi
A framework for formally verifying distributed systems implementations in Coq
Stars: ✭ 496 (+9820%)
Mutual labels: coq
crimp
Certified Relational to Imperative.
The goal of this project is a verified compiler from SQL-like queries to imperative code.
The core theorem statement is of a similar form to other translation equivalence theorems.
Theorem queryEquivalence:
forall (q : Query) (p : ImpProgram),
queryToImp q = Some p ->
forall (r1 r2 r' : relation), runQuery q r1 r2 = Some r' ->
runImp' p r1 r2 = Some r'.
Or
if the compiler accepts the query, and the query produces successful output according to the semantics of relational algebra(+), then the Imp program will succeed and produce the same output
Inspired by verifying transformations in Raco.
Dependencies
- Coq 8.4+ (tested at 8.4, may work with down to 8.2)
- Tactics from Certified Programming with Dependent Types
Get Coq dependencies
wget http://adam.chlipala.net/cpdt/cpdtlib.tgz
tar xf cpdtlib.tgz
cd cpdtlib
coqc CpdtTactics
Build Crimp
export CPDT_HOME=/path/to/cpdtlib
cd crimp
make
Run Crimp proofs
You can run the query equivalence proofs with
make QueryEquivalence.vo
or you can open QueryEquivalence.v in your favorite/un-favorite Coq environment, like Proof General.
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at [email protected].