Depuis l'automne 2008, je suis thésard en informatique théorique au LIX, le laboratoire d'informatique de l'Ecole Polytechnique (ce qui ne veut pas dire que je possède un sabre ou autre objet dangereux de ce genre). Je suis financé par une bourse du ministère (via l'EDX) et je travaille sous la direction de Lutz Straßburger, au sein de l'équipe Parsifal, où l'on fait des choses sympathiques, comme de la théorie de la preuve, de la programmation logique, et d'autres choses du genre en rapport avec la logique et les programmes (et le chef ici, c'est monsieur Dale Miller).
Vous ne pouvez pas me joindre par téléphone pour l'instant car je n'ai pas de téléphone fixe, bien que j'ai maintenant un bureau avec une place dedans (1019), donc utilisez plutôt les autres moyens disponibles, de préférence mail et ours-voyageur :
| par courrier : | Ecole Polytechnique |
|---|---|
| Laboratoire d'Informatique (LIX) | |
| rue de Saclay | |
| 91128 Palaiseau cedex (France) | |
| par mail : | nguenot at lix point polytechnique point fr |
Pour signer, crypter, ce genre de choses, ma clé GPG a pour identifiant 07A30F19 et repose sur le serveur subkeys.pgp.net ainsi que là.
Recherche
Attention ! Le monde de la recherche, c'est pas le bon vieux canapé de votre grand-mère ! Il s'y passe des choses pas forcément très chouettes... allez voir Sauvons La Recherche.
Dans la vie, je fais de la logique. Plus précisément, je fais de la théorie de la preuve et je tente des fois de l'appliquer à la programmation logique (waouh, comme je colle bien aux thèmes de mon équipe). En vrai je travaille sur la notion de focusing et sur les propriétés de permutabilité dans le calcul des séquents et dans un autre formalisme logique développé récemment (comme une alternative au calcul des séquents) qui s'appelle le calcul des structures. Et puis aussi d'autres choses liées de près ou de loin, comme les transformations de preuves et les proof-nets. Vous trouverez plus de détails sur ma page de recherche.
Centres d'intérêts
- Formalismes logiques : calculs des séquents, calcul des structures, proof-nets...
- Programmation logique et méthodes de construction automatique de preuves
- Démonstration automatique, assistants mathématiques (comme Coq ou Isabelle)
- Programmation fonctionnelle, lambda-calculs et isomorphisme de Curry-Howard
Articles
- Concurrency and Permutability in the Sequent Calculus - mai 2009, présenté à ESSLLI'09 dans le workshop satellite Structures and Deduction 2009 (pdf, slides)
Enseignement
Attention (encore) ! A la fac non plus, c'est pas toujours la joie... pour de l'info à propos de la réforme LRU et de la "privatisation" de l'université, allez voir Sauvons l'Université !
Je suis aussi moniteur à l'université Paris-Nord (UP13) à Villetaneuse, et j'assure des TDs et TPs du cours Eléments d'Informatique, organisé par Pierre Boudes et Erick Alphonse, qui sert d'introduction à l'informatique pour les étudiants de L1 et qui est principalement axé sur les bases du langage C et plus généralement la programmation impérative. Voir là.
Liens en vrac
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |