Translating Canonical SQL to Imperative Code in Coq
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
Explore a groundbreaking presentation on DBCert, the first mechanically verified compiler that translates SQL queries in canonical form to imperative code. Delve into the innovative contributions made by researchers Véronique Benzaken, Évelyne Contejean, Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, and Jerome Simeon. Learn about the complete translation from SQL to the Nested Relational Algebra, the development of Imp (a small imperative language for SQL targeting), and the mechanized translation process from nested relational algebra to Imp. Gain insights into how this work addresses divergences and bugs in SQL implementations, particularly in areas such as correlated queries and NULL value semantics.
Syllabus
[OOPSLA23] Translating canonical SQL to imperative code in Coq
Taught by
ACM SIGPLAN
Related Courses
Programming LanguagesUniversity of Virginia via Udacity Building a Basic Website
University of Massachusetts Amherst via Independent iDESWEB, Introducción al desarrollo web
Miríadax Web Engineering II: Developing Mobile HTML5 Apps
Technische Hochschule Mittelhessen via iversity Web Application Architectures
University of New Mexico via Coursera