Utabcert is a Coq formalization of equivalence and containment results obtained by Sagiv and Yannakakis (Equivalence Among Relational Expressions with the Union and Difference Operators).
Under the assumption of the results of a recent ESOP paper (A Coq Formalization of the Relational Data Model. V Benzaken, É Contejean, S Dumbrava.) it provides:
  • Formalization of the relational database model
  • Two notions of queries: union of conjunctive queries and monotonic relational expressions
  • Partly proven translation from monotonic relational expressions to conjunctive queries
  • Proof of the Homomorphism Theorem for union of conjunctive queries


Manager: Miriam Polzer, Tadeusz Litak

Developer: Lutz Schröder