coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] from FinType to Data Base
Date: Mon, 13 Dec 2021 12:48:47 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-qv1-f51.google.com
Ironport-data: A9a23:pNUk/q24vqyJA9uqI/bD5b1wkn2cJEfYwER7XOPLsXnJ0jslgjRWzTccX2/VP/6MM2X2eNslPtyxoRkAuJLXn9MSHQtv/xmBbVoa8JufXYzxwmTYZn7JcJWbFCqL1yivAzX5BJhcokT0+1H9YtANkVEmjfvRH+ClU7aeUsxMbVYMpBkJ2UoLd9ER2dYAbeiRW2thiPuqyyHtEAfNNw1cbgr435m+RCZH55wejt+3UmsWPpintHeG/5Uc4Ql2yauZdxMUSaEMdgK2qnqq8V23wo/Z109F5tKNl7/6dggTXOeXM1XXzHVRXKemj15JoSlaPqQTbqJNLxcKzW/QzpYskb2htrToIestFrXNlf4HXl9TFDxkIaxL5ZfIJHG+tYqYyEiun37Emq0wVB9mZdVwFuFfWDkSr5T0MgslZReawumy3biTUfhpns1lLc/xPYpZtGsI8N1zJeJ+FMqFHLGTsIcehCNq05gIR6ePPt5CPGIpMQCfNjRRHnwSLL4+uMahoEXlVwNZjUbM/f9uuyyI2GSdy5DoOdvRP8WUHIBbwx/eqWXB8GD0RBodMbSiJfO+2irErofycenTAur+1YFU98KGRHWWz20XTQQIDB61/KD/hUm5VNZSbUcT/0LCaIBaGFODFrHAs9+Q+RZofSLwn/JfFuQ77EeGza+8D8OxGD0fVjAYADA5nJZeeNHpv2NlW/vmADVutPueTnf1GnK8xd+tEXB9EFLurhPogefIDxcPbW3zYt/yog5fLZOI
Ironport-hdrordr: A9a23:woDyDqhXpM7N4rZPgZDmjV5NsHBQXjAji2hC6mlwRA09TyXPrbHWoB19726WtN9xYhEdcL+7U5VoLUm3yXde2/h3AV7BZmbbURqTTb2KhLGKqwEIfReSygc378ldmsZFZOEYJGIK9frS0U2XE8sEyNLC2Ly0hOHEpk0dKz1CWuVP7xpdAg3eK1ZxRwVNGPMCZfihz/sCiTq8XHwdKv2hAHoIVfWGh9CjruOCXTc2QzAm9SyHhneQ87j4HxKEmi4XTjIn+8ZHzVT4
Ironport-phdr: A9a23:JkCGzRJOFoLlxhwYlNmcuNZmWUAX0o4c3iYr45Yqw4hDbr6kt8y7ehCFvLM90xSQBM3y0LFts6LuqafuWGgNs96qkUspV9hybSIDktgchAc6AcSIWgXRJf/uaDEmTowZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF5Ovn5FpTdgsipyuy+4Z7ebgdHiDagfL95MQm7oxjWusQKm4VpN7w/ygHOontGeuRWwX1nKFeOlBvi5cm+4YBu/T1It/0u68BPX6P6f78lTbNDFzQpL3o15MzwuhbdSwaE+2YRXX8XkhpMBAjF8Q36U5LsuSb0quZxxC+XNtDtQLsqRTqt8btkSB7wiCcGKTE59n3Xitdth65fuR6tugBzz5LRbIyTKfFwfL7SfckCSGVOUMZeVSxPDI2/YYUSEeQOIelWopLhp1sXtxayGRWgCP/txzJOm3T43bc60+MkEQzexgIgHswBsG7OrNrrKawfT+e1zLTSzTXfbvNZxyr945XPfxA5oPGDQ6hwcdDPxkU1CwzFiUiQqZb5PzOUyOsNrnOW7+VlVe21im4nrxt9rSSoxscpk4TEgJ8exV/Y+ytj2ok1OcG4R1BhYd6iCJZdty6UO5Z3T888X2xlpTo2x6MIt5KmfCUH1ZAqygLQZfCbboSF4hLtWfqPLDp5hX9oZLGyihmv/EWvzuDxVsa63VBXpSRLldnMs2oC1x3V6sWfTvt95Eah1SyB1wDJ7OxPPEM6lbLDJpI/3rI9koAfvEfDEyPshkn6kaubel8k9+S17ensf6/oqYWGN4BujwHzKqQuldK7AeQ/KgUOWnKU+eW41LH65E35XqhGguQ4kqTZrZzWP8sbpqm+Aw9a1oYs9QyzACuh0NQdhXUHLVRFdwybj4XxJV3CPPT1Ae28jlmsijtn2e3KM7n7DpjNM3TPiLLhcqx8605Yxgoz19df55dMB7EZIfL8RFXxtMbGARMjLwO0xPvnCM9h1oMfR22PH7SUMKzXsVCS5+IvJ/OAa5MSuDb4M/Ql/eLhjWclmV8BeqmkxYcYaHehHvh/P0qZZWfsjcwaHGcRvgs+SfTqh0eYXT5SYXayRaM86SshBIKoF4eQDryq1ZeGxW+QGoBcLjRNDUnJGnP1fa2FXe0NYWScOJkyvCYDUO2ZSoI7zxzmnwjn0aZmI/ecrjUZuIj52Z5+4PDJiRA/6BR7Cs2c1yeGSGQizTBAfCM/wK0q+R818VyEy6UtxqUATbS7BttMWwY+cIfClql0Vom0VQXGcdOEDl2hR4f+adnUZt00yt4KJU16Hof65vgs9yWvCr4R0beMAc5tmp8=

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