coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] from FinType to Data Base

From: Alex Shkotin <alex.shkotin AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] from FinType to Data Base
Date: Mon, 13 Dec 2021 17:58:28 +0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=alex.shkotin AT gmail.com; spf=Pass smtp.mailfrom=alex.shkotin AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f182.google.com
Ironport-data: A9a23:y5Wo36pwCjSdQ7XBPMEECZFvzfteBmJwZBIvgKrLsJaIsI5as4F+vjZLWm6Gb/6INzejeI90bYS09RkHucWBnNVjQQA4qX09Zn8b8sCt6faxfh6hZXvKRiHgZBs6tJtGMoGowPjZ/xYwnz/1WlTahSQ6hfHgqobUUraeY3krHFQ8Ek/NtDo68wIHqt4w6TSGK1jV0T/Ci5W31G6Ng1aYAEpMg06wgE8HUMDJhd8tlgdWicanE7PpvyJ94Jo3fcldJpZjK2VeNrbSq+3rlNlV8o5FlirBBO9Jkp6jGqELarvbPAzLi34PHqb70kIEqSs13aI2cvEbbC+7iR3Tx4E3mIgL7MLuD155ZMUgm8xFO/VcOyh6ML0A47/EJmS+t+ScykTHdz3nxPAG4EQeZNVGpbYmWj8mGfswcWhRNHhvndmey7WiD+Jom84LN9juJIpZu3d6zDifA+xOfHxpa7GSsIUegyNp05gIReKEMpJfM2s+NQCbNkUJZ0NIXbsguMytolX/VxxRjm6PgZQ2xnyKlFkoi/y1JLI5YfSPTMRR20ec/yfIpjSjRB4dM9ObxHyO9XfEuwMGpgujMKp6KVFy3qU66LFS+oASNPHSfV6yoP38i0rnHtwGexZS9S0poqw/skesS7ERmjXQTGGs5nYhtxh4SoXWKz1hDoLb5g+YAi4PSTsphBkOqpotXTJzvrOWt4qBONGs2YF5jVqS876VqXW5Pi19waoqDcMbZVNt3uQPa73fQv4CohiP3UJ1YhDI9enM/g23
Ironport-hdrordr: A9a23:kmUmu6uHvoiMLQMZvpSOK0hn7skDT9V00zEX/kB9WHVpm62j5rmTdZEgvyMc5wxhPU3I9erwWpVoBEmslqKdgrNxAV7BZniDhILAFugLhrcKgQeBJ8SUzJ876U4PSdkZNDQyNzRHZATBjTVQ3+xO/DBPys6Vuds=
Ironport-phdr: A9a23:a1HMtBEmWAxj/Mkla0h+r51Gf9pMhN3EVzX9CrIZgr5DOp6u447ldBSGo6k31RmZAs6CsrptsKn/i+jYQ2sO4JKM4jgpUadncFs7s/gQhBEqG8WfCEf2f7bAZi0+G9leBhc+pynoeUdaF9zjaFLMv3a88SAdGgnlNQpyO+/5BpPeg9642uys5pHfeQZFiTiybb9vMRm9sBncuNQRjYZ+MKg61wHHomFPe+RYxGNoIUyckhPh7cqu/5Bt7jpdtes5+8FPTav1caI4TadFDDs9KGA6+NfrtRjYQgSR4HYXT3gbnQBJAwjB6xH6Q4vxvy7nvedzxCWWIcv7Rq0yVD+/7alkVQXohT8IOD438m7ZisJ+gqFGrhy/uxNy2JTbbJ2POfdkYq/RYdEXSGxcVchRTSxBBYa8YpMTAuoFI+lZoJT2qUYOrRu9AgmsGOLvyjlVjXLxx6I61/ouEA7c0Aw7H9IOs3PUrMn0NKcUSu21w6zIwi/Cb/NSwzvy9I/IchU4rPyKQLl/ftbfx1M1GAPZklWft5blPzWN2+kJsGWW7+puWO2hhWMmqgx9vyWjy8kihIXUh48bxF/J+Th7zYooJ9C2RlJ2bN6kHpZeuSyXNIp7TMwsTmx1tis3zKANt5C8fCgP0psnxhjfZuSDc4iS4xLvTuiRIS1giHJhYrK/hgy+/VKuyu3mUMS/zVVErjJdn9XSqnwA0wbf58uHR/dn40us2DeC2xrO5uxHP0w5k7fQJYQ7zb4qjJUTtFzOHi/ol0Xyi6+bbkAk9fKp6+Tje7nmp5ucO5JthgHwL6gjmdKzDf43MggJWGib9uC826P58ULlR7VKi+U6kqjfsJ/EOcQWvrC1DxNR34o56BuyDy2q3MkZkHQGNl5JZRGKg5bxN1HLOv/4DPO/g1q2kDdswvDLJqfuApHTIXnMirvhZrZ9601byAovzNBf4YlZCr4EIP3pW0/xsMbUAQM+Mwyx2+rnEsly1psCWWKTBa+UKL/dsViR5u42P+aMYJIVty3mJvg+5//uiGc5lkUHcamo25sXcnG4Ee58L0WXe3q/yusGRGwNp081SPHgoFyESz9aIXioDIwm4TRuIYarHc/4RoOqnL2HlHOyGpBGIHtGCVeQEHHAeICNWvNKYyWXdJwy2gcYXKSsHtdynSqlsxX3nuIPxg/89SgRtJal399wtbW7ffAa8DV1C4Gc1zjIQTgkxCUHQDg52K05qkt4mA/rOUdQjPlRFNgV7PRMAF5SCA==

Great!

Thank you,

Alex

пн, 13 дек. 2021 г. в 14:49, Pierre Courtieu <pierre.courtieu AT gmail.com>:

This work is about certiffication of database in coq:

Véronique Benzaken, Evelyne Contejean, Stefania Dumbrava:
A Coq Formalization of the Relational Data Model. ESOP 2014: 189-208

The linked project is here: http://datacert.lri.fr/

The latest version of the work I could find: http://datacert.lri.fr/sqlcert/

Best regards,
Pierre

Le lun. 13 déc. 2021 à 10:23, Alex Shkotin <alex.shkotin AT gmail.com> a écrit :
>
> Hi All,
>
> Is there any way to formalize the database if I need to prove the correctness of the Information System?
> finType sounds promising and is there any relational DB formalization done.
>
> Thank you,
>
> Alex
>

[Coq-Club] from FinType to Data Base, Alex Shkotin, 12/13/2021
- Re: [Coq-Club] from FinType to Data Base, Pierre Courtieu, 12/13/2021
  - Re: [Coq-Club] from FinType to Data Base, Alex Shkotin, 12/13/2021