===== Logiciels =====

=== Logiciels majeurs ===

    * [[https://www.irif.fr/~jch/software/babel/|Babel]]
    * [[http://www.cduce.org|CDuce]]  
    * [[https://galene.org/|Galène]]
    * [[https://coq.inria.fr|Coq]]
    * [[http://cshore.cs.rhul.ac.uk|C-SHORe]]
    * [[http://www.mancoosi.org/cudf/|CUDF]]
    * [[http://kappalanguage.org|Kappa]]
    * [[http://ocsigen.org/|Ocsigen]]
    * [[https://stamina.labri.fr/|Stamina]]
    * [[http://vaucanson-project.org/Awali|Awali]] · A generic C++-platform for computing with automata and transducers
    * [[https://usubalang.github.io/usuba/ |Usuba]]

=== Autres logiciels ===

  * [[https://www.irif.fr/~sighirea/celia|CELIA]] · Plugin for static analysis and verification of C programs with dynamic lists
  * [[http://mattam82.github.io/Coq-Equations/|Equations]] · Function definition by dependent pattern-matching and (well-founded) recursion in Coq
  * [[http://ocsigen.org/js_of_ocaml/|Js_of_ocaml]] · Compiler of OCaml bytecode in Javascript
  * [[https://ctan.org/pkg/knowledge|Knowledge]] · LaTeX package for the easy management of internal and external hyperlinks in a document
  * [[https://www.irif.fr/~vouillon/lwt/|Lwt]] · OCaml library for cooperative threads
  * [[http://gallium.inria.fr/~fpottier/menhir/|Menhir]] · Generator of OCaml parsers
  * [[https://github.com/colis-anr/morbig|Morbig]] · Parser for POSIX shell
  * [[http://www.lix.polytechnique.fr/Labo/Samuel.Mimram/rewr|Rewr]] · Library for algebraic rewriting
  * [[https://www.irif.fr/~jep/Logiciels/Semigroupe2.0/semigroupe2.html|Semigroupe]] · Computation of finite semigroups
  * [[https://www.irif.fr/~jch/software/homenet/shncpd.html|Shncpd]] · Implementation of a large subset of the Homenet protocol stack with minimal dependencies
  * [[https://www.irif.fr/~sighirea/spen/|SPEN]] · Solver for separation logic entailments
  * [[http://vaucanson-project.org/Vaucanson-g|Vaucanson-g]] · LaTeX macro package for drawing automata
  * [[https://plmlab.math.cnrs.fr/guiraud/catex|Catex]] · LaTeX tool to produce string diagrams for morphisms in free strict monoidal categories
  * [[https://github.com/ocaml/dune|Dune]] · Dune is a build system for OCaml
  * [[https://github.com/jscoq/jscoq|jsCoq]], [[https://github.com/ejgallego/pycoq|pyCoq]], [[https://github.com/coq/bot|CoqBot]]
  * [[https://github.com/ejgallego/coq-serapi|SerAPI]] · Library for machine-to-machine interaction, now replaced by [[https://github.com/ejgallego/coq-lsp|Coq LSP]]
  * [[https://mattam82.github.io/Coq-Equations/ |Equations]] · Equations provides a notation for writing programs by dependent pattern-matching and (well-founded) recursion in Coq
  * [[https://gitlab.com/irill/dose3|Dose3]] · Library and collection of tools to perform la large spectrum of analysis on package repositories
  * [[https://gitlab.com/nicolasbehr/ReSMT|ReSMT]] · An implementation of compositional rewriting theory algorithms



/*
  * [[https://www.irif.fr/~sighirea/celia|CELIA]] · Analyseur statique de programmes C avec structures dynamiques et allocateurs de mémoire, développé comme plugin de la plate-forme Frama-C
  * [[http://mattam82.github.io/Coq-Equations/|Equations]] · Définition de fonctions par filtrage dépendant et récursion bien fondée en Coq
  * [[http://ocsigen.org/js_of_ocaml/|Js_of_ocaml]] · Compilateur de bytecode OCaml en Javascript
  * [[https://ctan.org/pkg/knowledge|Knowledge]] · Package LaTeX pour la gestion facile d'hyperliens internes et externes ou de tables d'indexes
  * [[https://www.irif.fr/~vouillon/lwt/|Lwt]] · Bibliothèque OCaml pour les threads coopératifs
  * [[http://gallium.inria.fr/~fpottier/menhir/|Menhir]] · Générateur d'analyseurs syntaxiques OCaml
  * [[https://github.com/colis-anr/morbig|Morbig]] · Analyse syntaxique de scripts shell POSIX
  * [[http://www.lix.polytechnique.fr/Labo/Samuel.Mimram/rewr|Rewr]] · Bibliothèque de réécriture algébrique
  * [[https://www.irif.fr/~jep/Logiciels/Semigroupe2.0/semigroupe2.html|Semigroupe]] · Calcul de semigroupes finis
  * [[https://www.irif.fr/~jch/software/homenet/shncpd.html|Shncpd]] · Implémentation d'un sous-ensemble important du protocole Homenet
  * [[https://www.irif.fr/~sighirea/spen/|SPEN]] · Solveur pour la logique de séparation avec prédicats inductifs, pour la vérification de programmes manipulant des structures de données dynamiques
*/