A formalization of SQL with nulls

DOI10.1007/s10817-022-09632-4OpenAlexW3013999834MaRDI QIDQ2102947

James Cheney, Wilmer Ricciotti

Publication date: 12 December 2022

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2003.11331

zbMATH Keywords

SQLsemanticsCoqformalizationnulls

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Coq
• Kleisli
• HoTTSQL

Cites Work

• Unnamed Item
• Principles of programming with complex objects and collection types
• Normal forms and conservative extension properties for query languages over collection types
• Query lifting. Language-integrated query for heterogeneous nested collections
• Binding Structures as an Abstract Data Type
• On optimizing an SQL-like nested query
• SQL’s Three-Valued Logic and Certain Answers
• Strongly-Normalizing Higher-Order Relational Queries
• Toward a verified relational database management system
• Formal certification of a compiler back-end or
• A Coq Formalization of the Relational Data Model

This page was built for publication: A formalization of SQL with nulls