Software

 

Cette page liste les logiciels les plus importants pour lesquels le LIP est impliqué. La liste complète des logiciels enregistrés sur HAL est disponible à cette URL

  • GNU MPFR (ARIC): GNU MPFR est une bibliothèque de calcul à virgule flottante en multiprécision avec arrondi correct. Les calculs sont à la fois efficaces et bien définis sémantiquement. MPFR s’inspire des bonnes idées de la norme ANSI/IEEE-754 pour l’arithmétique à virgule flottante en double précision.

  • MPFI (ARIC): MPFI est une bibliothèque d’arithmétique par intervalles en précision arbitraire, basée sur MPFR et écrite en C.

  • gfun (ARIC): gfun est un package Maple qui fournit des outils pour manipuler les équations différentielles linéaires ou de récurrence linéaires comme des structures de données, ainsi que des outils pour deviner une telle équation à partir des premiers termes d’une suite ou série.

  • CTrees (CASH): A Rocq library for monadic models of non-deterministic, recursive, and effectful computations.

  • Dcc (CASH): Dcc (Data-aware process network C Compiler) compiles a regular C kernel to a data-aware process network (DPN), a dataflow intermediate representation suitable for high-level synthesis in the context of high-performance computing. Dcc has been registered at the APP (”Agence de protection des programmes”) and transferred to the XtremLogic start-up under an Inria license.

  • Dowsing (CASH): Dowsing is a tool to search function by types. Given a simple OCaml type, it will quickly find all functions whose types are compatible.

  • Math-Components (CASH): a set of Rocq libraries that cover the prerequisites for the mechanization of the proof of the Odd Order Theorem.

  • NetDiffusion (HowNet): NetDiffusion is a tool that uses a finely-tuned, controlled variant of a Stable Diffusion model to generate synthetic network traffic that is high fidelity and conforms to protocol specifications.

  • ENSnano (MC2): a 3D modeling software for DNA nanostructures

  • OS simulator (MC2): a fast and memory-efficient iPad app that simulates arbitrary Oritatami Systems (works with limitations on Apple silicon M1 too)

  • BenchOpt (OCKHAM): Benchopt is a benchmarking suite tailored for machine learning workflows. It is built for simplicity, transparency, and reproducibility. It is implemented in Python but can run algorithms written in many programming languages.

  • LazyLinOp (OCKHAM): LazyLinOp provides high-level linear operators based on an arbitrary underlying implementation, such as custom Python functions, NumPy-compatible array or butterfly Matrices.

  • Skglm (OCKHAM): skglm is a Python package that offers fast estimators for regularized Generalized Linear Models (GLMs) that are 100% compatible with scikit-learn. It is highly flexible and supports a wide range of GLMs. You get to choose from skglm’s already-made estimators or customize your own by combining the available datafits and penalties.

  • Click and Collect (Plume): An Interactive Linear Logic Prover. Online tool for constructing and transforming proofs in linear logic

  • EmergeNS (Plume): Simulation of chemical reactions and detection of autocatalytic cycles.

  • Yalla (Plume): Yet Another LL Library for Rocq (Linear Logic).

  • coinduction (Plume): A library for doing proofs by (enhanced) coinduction, based on the notion of ‘companion’. Reworked to take advantage ‘tower induction’.

  • graph-theory (Plume): A library of formalised graph theory results, including standard results from the literature (e.g., Menger’s Theorem, Hall’s Marriage Theorem, the excluded minor characterisation of treewidth-two graphs, and Wagner’s Theorem) as well as more recent results arising from the study of relation algebra (e.g., soundness and completeness of an axiomatisation of graph isomorphism)