Les réalisations de nos utilisateurs

Cette liste a été initialement recueillie par Basile Starynkevitch (Commissariat à l'Énergie Atomique, France).

• ASTREE est un analyseur statique de codes C qui établit l'absence d'erreurs run-time dans le logiciel critique embarqué. A été appliqué au logiciel de contrôle de vol des avions Airbus 340 et 380.
• SLAM est un outil d'analyse statique de programmes, développé chez Microsoft Research, pour détecter des erreurs dans les pilotes de périphériques Windows.
• Lindows, une distribution Linux, utilise plusieurs outils de gestion systèmes développés en OCaml. En voici une description.
• LexiFi développe des outils d'analyse financière et de pricing en MLFi, une extension d'OCaml.
• Le groupe de Frank Dellaert à Georgia Tech a écrit en Caml plusieurs applications de vision par ordinateur et de robotique. Vu sur CNN.
• ALVE Recorder est écrit en Objective Caml. Ce programme enregistre de façon digitale les appels téléphoniques. Contacter Matt Boyd mattwb78756@yahoo.com pour de plus amples informations. (Ce produit n'existe plus, victime du dot-com crash de 2000.)
• NBCi shopping a utilisé Objective Caml de manière intensive, d'une part dans les outils développés par Liquid Market pour extraire et indexer la base de produits, et d'autre part dans le moteur de gestion des transactions. (Ce produit n'existe plus, victime du dot-com crash de 2000.)
• Unison, un outil de synchronisation de fichiers entre p.ex. un portable et une machine de bureau, pour Unix et Windows.
• FFTW. FFTW est une bibliothèque C extrêmement rapide pour calculer des transformées de Fourier discrètes (TFD). Il utilise un puissant optimiseur symbolique écrit en OCaml pour, étant donné une taille N, générer du code C fortement optimisé pour calculer les TFD de taille N. FFTW a obtenu le prix Wilkinson 1999 pour le calcul numérique.
• Dwight VandenBerghe a utilisé Ocaml dans un produit de simulation financière, il écrit: It's a financial simulation system for actuaries, used to determine the valuation of life insurance companies. I used Ocaml for the compiler portion of the system, and C++ for the runtime engine, which has to be very fast.
• GeneWeb, logiciel de généalogie avec interface Web (Daniel de Rauglaudre, INRIA, France).
• Coq, démonstrateur de théorème pour la preuve de programmes (INRIA, France).
• Odyssée, différentiation automatique de programmes Fortran (INRIA, France).
• Caravan parallélisation automatique et analyse de programmes séquentiels et data-parallèles (Pierre Boulet, Univ. Lille 1 et Versailles, France).
• HOPS (transformateur de programme, University of the Federal Armed Forces Munich, D-85577 Neubiberg, GERMANY).
• Ensemble est un ensemble de protocoles et d'outils pour la programmation d'applications distribuées et coopératives (Mark Hayden, université Cornell, Etats-Unis).
• sE - synchronousEifel, outil pour la conception et la programmation de systèmes logiciels réactifs embarqués temps-réel (Dr. Reinhard Budde, German National Research Center for Information Technology, projets ESPRIT SYRF et CRISYS, Allemagne).
• Switchware Active Networking projects (Michael Hicks, Univ. of Pennsylvania, Etats-Unis): Active networks explore the idea of allowing routing elements to be extensively programmed by the packets passing through them. This allows computation previously possible only at endpoints to be carried out within the network itself, thus enabling optimizations and extensions of current protocols as well as the development of fundamentally new protocols. .
• Filtrage de réseaux (Joshua D. Guttman, Mitre Corporation, Boston, Etats-Unis).
• Ocaml comme langage de script, Ching-Tsun Chou (Intel Corp, Californie, USA).
• Pict langage expérimental basé sur le Pi-Calcul (Univ. Pennsylvannie, USA).
• Supervision de réseaux Gilles FALCON France Telecom (division des réseaux nationaux).
• Programmes bioinformatiques par Andrew Conway.
• Analyse formelle de protocoles cryptographiques au Stanford Research International, Computer Science Lab par David Monniaux.
• Hevea, Un traducteur rapide de latex vers html en Caml, (Luc Maranget).
• The aim of the system daTac is to do automated deduction in first-order logic with equality. Its speciality is to apply deductions modulo some equational properties of operators, such as commutativity or associativity-commutativity (AC). The deduction techniques implemented, based on resolution, paramodulation and term rewriting, have been proved refutationally complete in [RV95].
  daTac is written in Caml Light version 0.7 (20000 lines). Its interface is written in Tcl/Tk. It runs on Digital and Sun workstations.
• SPIKE. The SPIKE system is an automatic theorem prover for Horn equational logics. SPIKE has been developed in Nancy as part of the PROTHEO project (INRIA Lorraine and CRIN). Written in Caml Light, the program is provided with a graphic interface in TCL/TK that allows for interaction through the mouse and menus. SPIKE is designed for supporting the construction of correct specifications through verifying properties by induction.
• .... etc

Cette liste est très incomplète et en cours d'élaboration.