A Coq formalisation of SQL's execution engines

DOI10.1007/978-3-319-94821-8_6MaRDI QIDQ1791148zbMATH OpenOpenAlexFDO

Authors Yanyan Li

Publication date 4 October 2018

Full work available at URL https://doi.org/10.1007/978-3-319-94821-8_6

Mathematics Subject Classification ID

Database theory (68P15) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• A Coq formalization of the relational data model
• Toward a verified relational database management system
• A formalization of SQL with nulls
• scientific article; zbMATH DE number 1070623
• Certified Graph View Maintenance with Regular Datalog

Cited in

(4)

• A Coq formalization of the relational data model
• A formalization of SQL with nulls
• Toward a verified relational database management system
• A formally verified, optimized monitor for metric first-order dynamic logic

Describes a project that uses

Uses Software

• SEQUEL
• SQLCert
• Q*cert
• HoTTSQL
• CertiCoq
• CertiKOS
• Fiat
• Coq/SSReflect
• Why3
• Isabelle
• Coq

This page was built for publication: A Coq formalisation of SQL's execution engines

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1791148)