{"id":1209,"date":"2025-02-13T10:42:45","date_gmt":"2025-02-13T09:42:45","guid":{"rendered":"https:\/\/www.ens-lyon.fr\/LIP\/PLUME\/?page_id=1209"},"modified":"2025-02-13T11:22:03","modified_gmt":"2025-02-13T10:22:03","slug":"software","status":"publish","type":"page","link":"https:\/\/www.ens-lyon.fr\/LIP\/PLUME\/software\/","title":{"rendered":"Software"},"content":{"rendered":"\n<h2 class=\"wp-block-heading\">Non-Rocq software<\/h2>\n\n\n\n<ul class=\"wp-block-list\">\n<li><a href=\"https:\/\/github.com\/Kappa-Dev\/ReGraph\">ReGraph<\/a> : Python library for building graph-based hierarchical knowledge representation systems. Russ Harmer &amp; Eugenia Oshurko<\/li>\n\n\n\n<li><a href=\"https:\/\/github.com\/Kappa-Dev\/KAMI\">KAMI<\/a> : Bio-curation tool to construct executable models of signalisation paths in Kappa. Russ Harmer &amp; Eugenia Oshurko<\/li>\n\n\n\n<li><a href=\"https:\/\/github.com\/deniskup\/EmergeNS\">EmergeNS<\/a> : Simulation of chemical reactions and detection of autocatalytic cycles. Denis Kuperberg<\/li>\n\n\n\n<li><a href=\"https:\/\/perso.ens-lyon.fr\/damien.pous\/hypergraph\">Hypergraph<\/a> : Online tool to edit and analyse hypergraphs and their treewidth. Damien Pous<\/li>\n\n\n\n<li><a href=\"https:\/\/github.com\/ComputerAidedLL\/click-and-collect\">Click and Collect<\/a> : An interactive linear logic prover. Olivier Laurent &amp; \u00c9tienne Callies<\/li>\n\n\n\n<li><a href=\"https:\/\/github.com\/jonas-trms\/mll_prover\">MLL Prover<\/a> : Prototype of interactive prover with automatic context inference for MLL. Olivier Laurent &amp; Jonas Torriero-Meskour<\/li>\n<\/ul>\n\n\n\n<h2 class=\"wp-block-heading\">Tools and libraries for Rocq<\/h2>\n\n\n\n<ul class=\"wp-block-list\">\n<li><a href=\"https:\/\/github.com\/coq-community\/graph-theory\">graph-theory<\/a> : Library of formalised graph theory results. Damien Pous &amp; Christian Doczkal<\/li>\n\n\n\n<li><a href=\"https:\/\/github.com\/damien-pous\/relation-algebra\">relation-algebra<\/a> : Library and automation tactics for binary relations. Damien Pous &amp; Christian Doczkal<\/li>\n\n\n\n<li><a href=\"https:\/\/github.com\/damien-pous\/coinduction\">coinduction<\/a> : A library for doing proofs by (enhanced) coinduction. Damien Pous<\/li>\n\n\n\n<li><a href=\"https:\/\/github.com\/olaure01\/yalla\">Yalla<\/a> : Yet Another linear logic Library. Olivier Laurent<\/li>\n\n\n\n<li><a href=\"https:\/\/gitlab.inria.fr\/amahboub\/approx-models\">approx-models<\/a> : Library to verify rigorous approximations of univariate functions on real numbers. Damien Pous, Assia Mahboubi &amp; Florent Br\u00e9hard<\/li>\n\n\n\n<li><a href=\"https:\/\/github.com\/olaure01\/ollibs\">OLlibs<\/a> : Add-ons for the standard library. Olivier Laurent<\/li>\n\n\n\n<li><a href=\"https:\/\/github.com\/clucas26e4\/List_Permutation\">List Permutation<\/a> : Canonical representation for permutations and their action on lists. Olivier Laurent &amp; Christophe Lucas<\/li>\n\n\n\n<li><a href=\"https:\/\/github.com\/ComputerAidedLL\/FormalizedLLBib\">FormalizedLLBib<\/a> : Collection of formalisations of linear logic. Olivier Laurent<\/li>\n<\/ul>\n\n\n\n<h2 class=\"wp-block-heading\">Rocq formalisations<\/h2>\n\n\n\n<ul class=\"wp-block-list\">\n<li><a href=\"https:\/\/github.com\/RemiDiG\/proofnet_mll\">Proof nets for MLL<\/a>: Formalisation of multiplicative proof nets. Olivier Laurent &amp; R\u00e9mi Di Guardia<\/li>\n\n\n\n<li><a href=\"https:\/\/github.com\/olaure01\/quantifiers\">Quantifiers<\/a> : Formalisation of the \u201canti-locally nameless\u201d approach to quantifiers. Olivier Laurent<\/li>\n\n\n\n<li><a href=\"https:\/\/zenodo.org\/records\/4897193\">RieszRocq<\/a> : Formalization for the article &#8220;Free modal Riesz spaces are Archimedean: a syntactic proof&#8221;. Matteo Mio &amp; Christophe Lucas<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Non-Rocq software Tools and libraries for Rocq Rocq formalisations<\/p>\n","protected":false},"author":2,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-1209","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/www.ens-lyon.fr\/LIP\/PLUME\/wp-json\/wp\/v2\/pages\/1209","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.ens-lyon.fr\/LIP\/PLUME\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/www.ens-lyon.fr\/LIP\/PLUME\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/www.ens-lyon.fr\/LIP\/PLUME\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.ens-lyon.fr\/LIP\/PLUME\/wp-json\/wp\/v2\/comments?post=1209"}],"version-history":[{"count":6,"href":"https:\/\/www.ens-lyon.fr\/LIP\/PLUME\/wp-json\/wp\/v2\/pages\/1209\/revisions"}],"predecessor-version":[{"id":1223,"href":"https:\/\/www.ens-lyon.fr\/LIP\/PLUME\/wp-json\/wp\/v2\/pages\/1209\/revisions\/1223"}],"wp:attachment":[{"href":"https:\/\/www.ens-lyon.fr\/LIP\/PLUME\/wp-json\/wp\/v2\/media?parent=1209"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}