coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Alex Shkotin <alex.shkotin AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] from FinType to Data Base
- Date: Mon, 13 Dec 2021 12:23:12 +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-io1-f47.google.com
- Ironport-data: A9a23:/EZbJqLnQzLDFREDFE+Rs5QlxSXFcZb7ZxGrkP8bfHDqhWwjhGEEzmdLWG2PM/reMDf1fNh/Oou29R4BuZCHmqc2QQE+nZ1PZyIT+JCdXbx1DW+pYnjMdpWbJK5fAnR3huDodKjYdVeB4Ef9WlTdhSMkj/jRHOOnULSs1h1ZHGeIdg9x0XqPpMZi2uaEsfDha++8kYuaT//3YDdJ6BYoWo4g0J9vnTs01BjEVJz0iXRlDRxDlAe2e3D4l/vzL4npR5fzatE88uJX24/+IL+FEmPxp3/BC/ugm7f/N0wNG/vcYVfIhX1RVKyvxBNFo0Te0I5hbKtaORoR0mvX2YwuoDlOncTYpQMBN6nBiKIGUxpfDyB4FaJD8b7DZ3O4tKR/ymWfKyawn6s+XSnaOqVBorotaY1UztQTLylIZRSejcqt0bejQ69tgN4iJY/lJusiVttI2WmMV7B5VcmWG+OS8YUNhHFq15EXCa2LP4xEfWU6RQrkSBhrFlczKZsYoP2MuHjaZ2QA/QzR+r5fD3P7yQVw1P3sN4OQdIDVA8pSmUmcqyTN+GGRP/3TD/THoRLtz55mrrWnceLHtIMu+HmQ8/drhBiSwTVWBkFJE1S8pva9hwi1XNc3x4k8ksYxhfBayaBpZoCVs96ETLqssRsVWt4WGOo/gO1I4rSB+B6XXwDoURYYAOHLd6YKqfgC2VqAntevDjtq2FFQYRpx6Z/MxQ6P1eMpwaPuqMPKocbpIzUunW3rsi/ycw==
- Ironport-hdrordr: A9a23:wuLnq61jS83PCTbS+mnkcAqjBFgkLtp133Aq2lEZdPUCSL3gqynIpoV56faUslYssR4b8uxoVJPrfZr3z+8T3WByB9iftXjd2VdARbsKhbcKpQeMJ8SUzIBgPMlbH5SWIeeAdWRSvILV4BScG91l6MWb8aay7N2uqUtFfEVFa7xE5ww8Mx2cEUF9WWB9dPgEPavZyMpbgjKqPU0NaMe2DGRAf+WrnayvqLvWJTAHGjsu4022ljWq5LTmVyGRwxZ2aUIq/Ysf
- Ironport-phdr: A9a23:hu8jqBcCWqw14HnDk2txPPHhlGM+st7LVj580XLHo4xHfqnrxZn+JkuXvawr0AWQG9WEoKsdw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94PObwlShzewY7x+IAiroQ7MqsQYnIxuJ7orxBDUuHVIYeNWxW1pJVKXgRnx49q78YBg/SpNpf8v7tZMXqrmcas2S7xYFykmPHsu5ML3rxnDTBCA6WUaX24LjxdHGQnF7BX9Xpfsriv3s/d21SeGMcHqS70/RDKv5LppRhD1kicKLzE2/mHZhMJzkaxVvg6uqgdlzILIeoyYLuZycr/fcN4cWGFPXtxRVytEAo6kc4YPC/QOPOlFpIfgp1sOrhy+BRWtBOPp1zRFgWX53akk3OUuCw3GxwwgH9EJsHTIrdX1MrwfUe+wzKbSzDXDa+la1iv66IjNax0sp+yHUr1sf8TL00YvCx/FgUuKqYzjJz6ZyOQDvWiG4+dhSO+jlnIqpxxtrjSx2Mogl5XFi4AVxF3Z8Sh0wIQ4KN2mREN5Y9OpEZ9duz+VOYZ3Qs0vXX9ltSAnwbMFoZ62ZDYGxIgjyhLFaPGKc5KE7g/iWeuQOzt1i3BodbSijBio60eg0PfzVsys3VZKsCVFlt7Mu2gI1xPJ68iHTuJx/kam2TqSzgzT5O5JLEIumarULJ4hxbEwlp4NvkjZAiD2n0D2gLeXdkUi5Oeo9/zqbqv6qpKYLYN5iQHzPr4zlsG+AOk0KAcDUmqD9eS5zrLj/En5QLtQjv0xl6nUqIrVJcAFqa+2GQNVyYYj6xW4Dze60dQYm2IKLF1AeB2djojpP0vCL+z/Dfe6m1isiitkx+jaPr39BZXANmTMkLD4fbpk90FczBczwstE6pJPCrABJerzVVXruNzZCB85KQ20zPz9BNVzzINNEV6IV6SeKebZtUKCzuMpOeiFIoEP6xjnLP1wzvrjnTcCmVwaYaivlc8ebH2oWO9mIEKFYHzEjdIIEGNMtQ07Gr+5wGaeWCJeMi7hF5k34Ss2XdrO5WjrSYWkgbjH1yC+TMQ+joFuD1mNFTLpcNzBVatTLi2VJcBln3oPUr3zE+fJMDmhsQb7z/xsKe+GokUl
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
- Re: [Coq-Club] from FinType to Data Base, Pierre Courtieu, 12/13/2021
Archive powered by MHonArc 2.6.19+.