Logiciels

 

Tac/μLJ: focused inductive theorem proving

Tac is a framework for implementing interactive theorem provers with good support for both interactive proof development and automated proof search. In that framework, we implemented a focusing proof system for μLJ, i.e., intuitionistic logic with least and greatest fixed points. We showed that a relatively naive proof search procedure, built on the refined foundations provided by focusing, yields surprisingly good results. This tool also implements the lifting approach to generic quantification (cf. research paper). Learn more on the Slimmer page of tac.

Bedwyr: a proof-search approach to model-checking

Bedwyr is a logic programming language which relies on the proof-theoretic notion of fixed point definition to support an operational reading of the implication as an exhaustive case analysis. It supports λ-tree syntax (a variant of HOAS), higher-order pattern unification and generic quantification (∇). It also uses tabling to handle (co)inductive specifications in a meaningful way. Examples of use include the verification of bisimulation for the π-calculus, exploration of winning strategies for games, properties of graphs/automata... in a purely declarative way. It is available through the INRIA gforge page of the Slimmer project. (See also in my publications, the one on Bedwyr.)

Savonet/Liquidsoap

Savonet est un groupe de développeurs, initialement Samuel Mimram et moi, puis une promo de l'ENS Lyon, et maintenant plusieurs développeurs de divers horizons. Nous travaillons depuis 2003 autour du streaming audio, en particulier pour des radios web. Notre générateur de flux, liquidsoap, est d'une flexibilité et d'une richesse inégalées, grâce à son architecture interne (en OCaml) et à son interface sous forme d'un langage de script dédié. Le projet Savonet est aussi à l'origine de nombreux bindings pour OCaml: vorbis, mad, shout, etc. Plus d'info sur la page officielle du projet. (Voir aussi dans mes publications pour plus de lecture.)

Petits outils

OMLet

Mon mode d'indentation OCaml pour VIm mérite maintenant une page pour lui tout seul.

Orienter ses photos numériques

Les appareils photos numériques enregistrent leur orientation lors des prises de vue, mais ne tournent pas les photos en fonction. Je me suis écrit flipper pour tourner les photos dans le bon sens après les avoir téléchargées sur mon ordi. (Juin 2004)

Galerie photo

J'ai aussi créé un système de galerie photo de plus. Ce n'est pas le plus simple au monde mais je le trouve joli et il me permet de modifier facilement le site.

Frontend pour jumpnbump

Un frontend pour le super jeu jumpnbump : jnbsync. Il permet aux clients de ne pas posséder le level que le serveur choisit, et évite d'attendre à l'infini un client qui ne veut plus venir. Bref, c'est plus pratique, et c'est léger. (Octobre 2003)

Tresses

Braidtex : un outil pratique produisant de jolis dessins de tresses au format EPS. On peut lui décrire une tresse de façon précise (du point de vue du dessin) ou par sa signature. (Été 2003)

Dyndns

Ddtun se charge de mettre à jour votre IP auprès de dyndns.org, qui se charge gratis de vous donner un nom de domaine. (Avril 2003)

Xchat

Watching est un plugin qui beep bien sous xchat. (Mars 2003)

Projets d'études

CUL

Second projet de programmation en OCaml : l'interpréteur Lisp CUL -- Caml Ultimate Lisp. Il supporte la curryfication, la récursion terminale, l'évaluation paresseuse, et les modes de liaison dynamique (emacs lisp) et statique (scheme, clisp). On a porté une attention particulière à l'architecture du code OCaml. Allez voir le CVS sur Sourceforge. (Janvier 2003)

FractCompr

Premier projet de programmation en OCaml : compression fractale. Allez voir le CVS sur Sourceforge. (Novembre 2002)

Spitch

Mon TIPE, sur la transcription graphème-phonème : tout, la doc en pdf, ou juste les sources (C++) des programmes sans même le dictionnaire BRULEX, utilisé par spitch. Dispo aussi, la version de l'époque des concours. (Été 2002)

Projets presque oubliés

Choz

ChoZ est une application un peu dure à définir : "simulateur de monde ?". ChoZ fonctionne par plugins et définit un cadre souple : tout ce qui se représente en 2D. Je l'ai créé pour observer l'évolution de petits robots avec des réseaux de neurones éduqués par algos génétiques (la totale classique) pour explorer un labyrinthe le plus loin possible. L'interface graphique est réalisée grâce à Gtk-1, ça date un peu. Il y a peut-être de quoi vous amuser. Jetez un oeil à la capture d'écran puis la doc. (2001, corrigé en 2003)

Life

Une implémentation du célèbre jeu de la vie de John Conway, avec modification possible des règles. Utilise le Gtk-1,dispo en .tar.bz2. (2001, corrigé en 2003)