{"id":4,"date":"2011-12-08T11:55:34","date_gmt":"2011-12-08T11:55:34","guid":{"rendered":"http:\/\/project.inria.fr\/template1\/?page_id=4"},"modified":"2023-07-30T19:42:17","modified_gmt":"2023-07-30T17:42:17","slug":"home","status":"publish","type":"page","link":"https:\/\/project.inria.fr\/from23\/","title":{"rendered":""},"content":{"rendered":"<div class=\"wp-block-file\"><a id=\"wp-block-file--media-2d44c811-ef5e-44b5-b95c-9436837fd06a\" href=\"https:\/\/project.inria.fr\/from23\/files\/2023\/07\/coq.tar.gz\">coq.tar.gz<\/a><a href=\"https:\/\/project.inria.fr\/from23\/files\/2023\/07\/coq.tar.gz\" class=\"wp-block-file__button\" download aria-describedby=\"wp-block-file--media-2d44c811-ef5e-44b5-b95c-9436837fd06a\">Download<\/a><\/div>\n\n\n\n<p>Uses Coq <strong>8.17.0<\/strong> and its standard libraries enabling classical mathematical reasoning<\/p>\n\n\n\n<p><em>Instructions<\/em>: <\/p>\n\n\n\n<p><strong>gunzip coq.tar.gz<\/strong> ; <strong>tar xvf coq.tar<\/strong>;  <strong>cd coq <\/strong>; <strong>make<\/strong><\/p>\n\n\n\n<p><em>Contents<\/em>:<\/p>\n\n\n\n<p><strong>Oracle.v:<\/strong> in classical logic, every proposition or its negation holds<\/p>\n\n\n\n<p><strong>Sets.v<\/strong>, <strong>Poset.v<\/strong>, <strong>PPO.v<\/strong>, <strong>CPO.v<\/strong>, <strong>Ideal.v<\/strong>, <strong>Algebraic.v<\/strong>, <strong>Exp.v<\/strong>; <strong>Embedding.v<\/strong>:<br>infrastructure for sets, posets, PPOs, CPOs, ideals, algebraic CPOs, embeddings, and exponentials<\/p>\n\n\n\n<p><strong>Flifting.v<\/strong>: lifting a monotonic function between PPOs to a unique continuous function between respective embeddings of the PPOs<\/p>\n\n\n\n<p><strong>Conat.v<\/strong>, <strong>Option.v<\/strong> : infrastructure for the conat and option types<\/p>\n\n\n\n<p><strong>Monad.v<\/strong> : the reader and termination state monads<\/p>\n\n\n\n<p><strong>Partial.v<\/strong> : partial recursive functions<\/p>\n\n\n\n<p><strong>While.v<\/strong> : defining the while loop as a partial recursive function<\/p>\n\n\n\n<p><strong>Hoare.v<\/strong> : Hoare logic<\/p>\n\n\n\n<p><strong>LinkedList.v<\/strong> : the type of linked lists and its properties<\/p>\n\n\n\n<p><strong>Length.v<\/strong> : the case study about the length of linked lists.<\/p>","protected":false},"excerpt":{"rendered":"<p>Uses Coq 8.17.0 and its standard libraries enabling classical mathematical reasoning Instructions: gunzip coq.tar.gz ; tar xvf coq.tar; cd coq ; make Contents: Oracle.v: in classical logic, every proposition or its negation holds Sets.v, Poset.v, PPO.v, CPO.v, Ideal.v, Algebraic.v, Exp.v; Embedding.v:infrastructure for sets, posets, PPOs, CPOs, ideals, algebraic CPOs, embeddings,\u2026<\/p>\n<p> <a class=\"continue-reading-link\" href=\"https:\/\/project.inria.fr\/from23\/\"><span>Continue reading<\/span><i class=\"crycon-right-dir\"><\/i><\/a> <\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"open","template":"","meta":{"footnotes":""},"class_list":["post-4","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/project.inria.fr\/from23\/wp-json\/wp\/v2\/pages\/4","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/project.inria.fr\/from23\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/project.inria.fr\/from23\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/from23\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/from23\/wp-json\/wp\/v2\/comments?post=4"}],"version-history":[{"count":26,"href":"https:\/\/project.inria.fr\/from23\/wp-json\/wp\/v2\/pages\/4\/revisions"}],"predecessor-version":[{"id":103,"href":"https:\/\/project.inria.fr\/from23\/wp-json\/wp\/v2\/pages\/4\/revisions\/103"}],"wp:attachment":[{"href":"https:\/\/project.inria.fr\/from23\/wp-json\/wp\/v2\/media?parent=4"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}