{"id":31,"date":"2017-06-14T09:22:54","date_gmt":"2017-06-14T09:22:54","guid":{"rendered":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/?page_id=31"},"modified":"2017-06-28T09:19:19","modified_gmt":"2017-06-28T09:19:19","slug":"compilation-de-requetes-sql-de-bases-de-donnees-et-specification-extreme-en-coq","status":"publish","type":"page","link":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/?page_id=31","title":{"rendered":"SQL fait ses preuves"},"content":{"rendered":"

<\/p>\n

V\u00e9ronique Benzaken<\/a>, \u00e9quipe VALS<\/a>, LRI<\/a>, universit\u00e9 Paris-Sud Orsay<\/p>\n

Les donn\u00e9es sont omnipr\u00e9sentes et pr\u00e9cieuses. De fa\u00e7on surprenante peu d’attention a \u00e9t\u00e9 consacr\u00e9e pour garantir, de mani\u00e8re indiscutable, que les syst\u00e8mes en charge de leurs traitements sont s\u00fbrs. Une approche prometteuse afin d’obtenir des garanties fortes est d’utiliser des assistants \u00e0 la preuve tels que Coq.<\/p>\n

Dans cette conf\u00e9rence nous nous int\u00e9resserons aux syst\u00e8mes relationnels qui sont parmi les plus r\u00e9pandus et tout particuli\u00e8rement \u00e0 la cha\u00eene de compilation de SQL. Nous d\u00e9crirons les diff\u00e9rentes \u00e9tapes indispensables \u00e0 l’obtention d’une cha\u00eene de compilation certifi\u00e9e : sp\u00e9cification extr\u00eame, en Coq, du mod\u00e8le relationnel, m\u00e9canisation, en Coq, de la s\u00e9mantique de SQL, analyse syntaxique et s\u00e9mantique certifi\u00e9e et optimisation v\u00e9rifi\u00e9e.<\/p>\n

Si SQL est l’un des langages les plus utilis\u00e9 dans le monde \u2014 il est seulement d\u00e9pass\u00e9 par Javascript et figure loin devant C et C++ \u2014 c’est aussi l’un des langages le plus redout\u00e9 et le moins appr\u00e9ci\u00e9 des programmeurs. Nous tenterons, au cours de la pr\u00e9sentation, d’expliquer, \u00e0 la lumi\u00e8re implacable port\u00e9e par Coq, pourquoi.<\/p>\n

 <\/p>\n","protected":false},"excerpt":{"rendered":"

V\u00e9ronique Benzaken, \u00e9quipe VALS, LRI, universit\u00e9 Paris-Sud Orsay Les donn\u00e9es sont omnipr\u00e9sentes et pr\u00e9cieuses. De fa\u00e7on surprenante peu d’attention a \u00e9t\u00e9 consacr\u00e9e pour garantir, de mani\u00e8re indiscutable, que les syst\u00e8mes en charge de leurs traitements sont s\u00fbrs. Une approche prometteuse afin d’obtenir des garanties fortes est d’utiliser des assistants \u00e0 la preuve tels que Coq. […]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-31","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=\/wp\/v2\/pages\/31","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=31"}],"version-history":[{"count":4,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=\/wp\/v2\/pages\/31\/revisions"}],"predecessor-version":[{"id":61,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=\/wp\/v2\/pages\/31\/revisions\/61"}],"wp:attachment":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=31"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}