Qui suis-je ?

Mon portrait

Qui suis-je ?

Je suis un ancien chercheur postdoctoral dans l'équipe Max du laboratoire d'informatique de l'École Polytechnique (LIX), financé par une convention Digitéo.

Voir aussi mon cv.

Que fais-je ?

GNU TeXmacs

Je développais le logiciel GNU TeXmacs. Il s'agit d'un logiciel libre d'édition structurée pour le monde scientifique. Il a pour objectif de fournir un cadre homogène et ergonomique pour l'édition de documents composés de différents type de contenus (texte, mathématiques, graphiques, sessions interactives, etc.) avec une haute qualité typographique.

J'ai commencé à travailler sur GNU TeXmacs en tant qu'ingénieur. Il s'agissait essentiellement d'améliorer l'interopérabilité de ce dernier avec LaTeX. De nombreux développements ont été fait dans ce sens, et le logiciel à grandement progressé à ce niveau.

DoCoq

Les interfaces des assistants de preuves sont souvent très techniques à utiliser, et ne correspondent pas toujours à la façon dont travaille un mathématicien. Si on prend le cas de Coq, par exemple, l'utilisateur est notamment confronté à i) une interface en seul texte unicode ; ii) avec une écriture unidimensionnelle (et souvent non conventionnelle) des mathématiques ; iii) avec un processus de rédaction particulièrement linéaire : il n'est pas possible de poursuivre l'écriture d'un résultat sans avoir prouvé un énoncé donné (c-à-d repousser à plus tard la preuve d'un énoncé ; donc mener un processus de rédaction non-linéaire).

L'objectif de ce projet est d'expérimenter et développer une interface entre GNU TeXmacs et Coq tenant compte des critiques précédantes ; donc, utilisant tant que possible le langage et les notations usuelles aux mathématiciens, et permettant un fonctionnement plus local, permettant une rédaction plus « naturelle ».

Logiciel libre — April

Le logiciel fait tourner les machines qui font tourner le monde. Or, dans un monde où l'exercice des libertés fondamentales passe de plus en plus par l'usage des ordinateurs, nous devons nous préoccuper de qui contrôlent ceux-ci ; donc de qui écrit le logiciel et dans quel but.

Librement accessibles à tous, les logiciels libres sont écrit dans une logique ouverte à tous, auditables par tous, et largement accessibles à tous. Leur but premier est de garantir les libertés à l'ère de l'informatique.

Ils sont, par ailleurs, un bien commun qui contribut à rétablir l'égalité des chances en matière de technologies de d'information. Vecteurs d'émancipation ancrés dans un mouvement de partage de la connaissance, ils sont une opportunité pour la société à l'ère du numérique.

L'April est la principale association qui promeut et défend le logiciel libre en France.

Où suis-je ?

Adresse physique

 

Adresse postale

LIX - UMR 7161
École polytechnique
91 128 Palaiseau Cedex
France