8000 GitHub - ckeller/sqlfs: SQL formal semantics with some extensions

More Web Proxy on the site http://driver.im/

ckeller / sqlfs Public

forked from RadimBaca/sqlfs

Notifications You must be signed in to change notification settings
Fork 0
Star 1

SQL formal semantics with some extensions

1 star 2 forks Branches Tags Activity

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 14 Commits
src		src
.gitignore		.gitignore
AUTHORS		AUTHORS
LICENSE		LICENSE
Makefile		Makefile
README.md		README.md
coq-sqlformalsemantics.opam		coq-sqlformalsemantics.opam

Repository files navigation

SQLFormalSemantics

A Coq mechanized executable formal semantics for realistic SQL queries.

Compilation

This work compiles with Coq 8.15.0:

make
make install

License

This code is released under the terms of the Creative Common Attribution-NonCommercial-NoDerivatives 4.0 International license; see LICENSE for details.

Companion paper

A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra, Benzaken, Véronique; Contejean, Évelyne, CPP - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs - 2019

About

SQL formal semantics with some extensions

Report repository

Releases

No releases published

Packages

No packages published

Languages

Rocq Prover 97.8%
Makefile 2.2%

0