Page professionnelle de Clément Aubert

Contact

Une photographie, vous me reconnaîtrez à ma voix sinon ? Clément Aubert
Computer Science Department
Appalachian State University

Neuves

mar. 22 mars 2017

Mon site rebascule vers aubert.perso.math.cnrs.fr, que j’estime être plus stable que mon ancienne adresse au LACL. Merci à Nicolas Herniou d’avoir maintenu cet espace acceuillant et à jour!

mer. 1er mars 2017

Je serai l’année prochaine assistant professor à l’Augusta University, au Hull College. J’y aurai pour collègue notamment Harley Eades III, et narre comment j’ai candidaté aux postes tenure track.

De façon tout à fait invisible pour vous, ce site est désormais rédigé en markdown et emploie pandoc, si vous êtes curieux, direction ces notes.

Enfin, je vous renvoie désormais à dissem.in pour obtenir des versions auto-archivées de mes publications.

mer. 24 août 2016

Les enseignements ont commencé ici à l’Appstate, et j’enseigne cette année « CS 1440 », soit une classe d’intro à Java.

Côté recherche, notre papier Contextual equivalences in configuration structures and reversibility est en voie de publication, et je suis désormais reviewer pour l’American Mathematical Society et zbMATH.

jeu. 23 juin 2016

Grâce à l’obtention d’une bourse « Research Development Travel Grant », j’ai pu aller rendre visite à la NSF, à Arlington, afin de mieux comprendre comment candidater aux programmes de la NSF. Le compte-rendu de la visite est en ligne.

jeu. 12 mai 2016

Ioana Cristescu et moi avons révisé notre soumission au numéro spécial ICE 2015 de Journal of Logical and Algebraic Methods in Programming, Contextual equivalences in configuration structures and reversibility. Sinon, la version définitive de Logarithmic Space and Permutations, rédigé avec Thomas Seiller, a été publiée chez Information and Computation récemment.

lun. 4 avr. 2016

Les actes de FOSSACS 2016, contenant Unary Resolution: Characterizing Ptime, ont été publiés. C’est également le cas de Characterizing co-NL by a group action, publié en version papier chez Mathematical Structures in Computer Science.

mer. 3 fév. 2016

J’ai été invité à être membre du comité de programme de LCC, qui se tiendra cette année à Marseille, aux côtés de CSL. Je serai également présent, du 13 au 18 mars, à l’atelier From Theory to Practice of Algebraic Effects and Handlers, qui se tiendra à Dagstuhl. Enfin, notre article Logarithmic Space and Permutations, avec Thomas Seiller, est disponible en ligne.

dim. 20 déc. 2015

Alors qu’une collaboration avec Fredrik Nordvall Forsberg et Patricia Johann prends doucement forme, j’ai la joie d’apprendre que Unary Resolution: Characterizing Ptime a été accepté à Fossacs 2016. Les candidatures continuent, comme en témoignent un research statement et un teaching statement.

lun. 16 nov. 2015

Contextual equivalences in configuration structures and reversibility, rédigé avec Ioana Cristescu, a été soumis au Journal of Logical and Algebraic Methods in Programming, pour leur numéro spécial faisant suite à ICE 2015.

mar. 24 oct. 2015

Je travaille désormais à Boone, en Caroline du Nord, au département Computer Science de l’Université des Appalaches. J’ai rédigé quelques notes pour qui voudrait venir me voir et rédigé un site minimal en Anglais.

Nous avons soumis, avec Marc Bagnol et Thomas Seiller, Unary Resolution: Characterizing Ptime à Fossacs 2016.

lun. 24 août 2015

Les actes de ICE 2015, qui contiennent Reversible Barbed Congruence on Configuration Structures, ont été publiés. Nous avons été invités, avec Ioana Cristescu, à soumettre une version étendue de ce travail au numéro spécial ICE 2015 à paraître chez Journal of Logical and Algebraic Methods in Programming.

jeu. 4 juin 2015

Ce sera demain la quatrième fois en deux semaines que nous présentons avec Ioana Cristescu notre travail, Reversible Barbed Congruence on Configuration Structures. Je serai l’année prochaine à Boone, en Caroline du Nord, pour travailler au département Computer Science de l’ Appalachian State University avec Patricia Johann sur des questions de paramétricité relationnelle.

jeu. 7 mai 2015

Notre article avec Ioana Cristescu, Reversible Barbed Congruence on Configuration Structures a été accepté à ICE 2015. Nous avons enfin terminé, avec Marc Bagnol, une version journal de Unification and Logarithmic Space, que nous soumettons au numéro spécial de LMCS pour RTA/TLCA 2014.

lun. 2 mar. 2015

Alors que frémissent les postes d’ATER et de maître de conférence, je me décide à mettre quelques notes relatives au dossier LaTeX pour les concours de l’INRIA. Sinon, Gilles Dowek a proposé à Marc Bagnol et moi de reprendre notre papier RTA-TLCA 2014 pour un numéro spécial à paraître chez LMCS.

ven. 27 fév. 2015

L’exposé proposé à DICE a été accepté, je serai donc à Londres pour ETAPS 2015 du 11 au 16 avril. Sinon, je suis désormais qualifié pour le corps de Maître de conférence aux sections 25 (Mathématiques) et 27 (Informatique).

lun. 9 fév. 2015

Qu’on se le dise : le paquet ebproof d’Emmanuel Beffara est en version 1.0. C’est probablement l’outil que vous cherchez pour saisir de beaux arbres de dérivation en LaTeX.

Un exemple de dérivation et son code (simple).

jeu. 5 fév. 2015

Je serai demain à la réunion de lancement de l’ANR ELICA, à Paris 13. J’y ferai un exposé reprenant une un récent travail soumis à DICE 2015.

mer. 21 jan. 015

Je mets en ligne Memoization for Unary Logic Programming: Characterizing Ptime, co-rédigé avec Marc Bagnol et Thomas Seiller, et soumis à LICS 2015. J’en profite pour rédiger un mémo sur comment rendre son .tex portable.

jeu. 8 jan. 015

Notre article Logarithmic Space and Permutations, avec Thomas Seiller, a été accepté à Information and Computation — Special Issue on Implicit Computational Complexity.

Sinon, j’ai enfin trouvé un article qui prouve que MLL avec des axiomes atomiques et Logspace-complet, c’est dans Relating complexity and precision in control flow analysis (en ligne chez Henri Mairson).

ven. 5 déc. 014

Notre article Characterizing co-NL by a group action, avec Thomas Seiller, a été publié aujourd’hui même en first view chez Mathematical Structures in Computer Science.

ven. 14 nov. 014

Je compile quelques notes dans un recoin de ce site, et viens d’y ajouter un mémo sur comment accéder à un article. La question est brulante, entre destruction de bibliothèques (archive) et contrat record du ministère de la Recherche de France avec Elsevier (archive). La liste de la communauté francophone du libre accès, qui m’a gentiment été signalée par Anna Wojciechowska, témoigne de l’actualité de la question.

ven. 7 nov. 014

Deux choses: je publie (enfin) un errata à ma thèse. Une partie de la correspondance entre ATM et circuits de preuves était erronée. Vous pouvez retrouver cet errata dans une version mise à jour de ma thèse. Sinon, j’aurai le plaisir d’effectuer un exposé, intitulé « Naissance d’une approche sémantique de la complexité », lors de la prochaine réunion logoi.

lun. 6 oct. 014

D’aucuns cherchent à tout prix à avoir un CDI d’enseignant-chercheur, d’autres alertent en démissionnant… (archive).

jeu. 2 oct. 014

Je serai membre de comité de programmation de Dice 2015. Sinon, nouvelles adresses pour mon site (…), mon courriel (…) et mon bureau (situé au Campus Central de Créteil) : je suis désormais à Université Paris-Est Marne-la-Vallée et employé par l’Inria. J’animerai d’ailleurs le séminaire du LACL le lundi 20 octobre à 14 heures.

jeu. 7 août 014

Notre article Logic Programming and Logarithmic Space a été accepté à APLAS. Super, je peux mettre à jour mon c.v..

jeu. 24 juilet 014

Je serai l’année prochaine post-doc au Laboratoire d’Algorithmique, Complexité et Logique à l’Université Paris-Est Créteil Val de Marne, dans le cadre de l’ANR REVER, avec Jean Krivine et Daniele Varacca. D’ici là, l’été est studieux et je prépare quelques notes sur les automates et leurs rapports avec les classes de complexité qui me plaisent bien ( L, NL et P).

mar. 10 juin 014

Je mets en ligne Logic Programming and Logarithmic Space, fruit d’une collaboration entre quatre jeunes doctorants ou docteurs. Cet article sera le sujet des prochains séminaires que j’animerai. J’ajoute également les fichiers sources de différents articles.

mer. 15 mai 014

J’animerai le 12 juin le séminaire de mon équipe, et 19 juin le séminaire de l’équipe LIMD du LAMA, retrouvez tout le détail plus bas. Sinon, je continue et organise mon entreprise de prise de notes pratiques.

mar. 8 avr. 014

Notre article Unification and Logarithmic Space, avec Marc Bagnol, a été accepté à RTA/TLCA 2014.

lun. 7 avr. 014

Je mets en ligne quelques notes concernant les listes de di(ffu|scus)sion dans mon domaine.

lun. 10 mar. 014

Mon courriel est désormais …, et la version finale de ma thèse est désormais en ligne, sur cette page et chez tel. J’animerai le 19 mars le séminaire du département « Méthodes formelles » du Loria, retrouvez toutes les informations plus bas.

ven. 24 jan. 014

Veuillez mettre à jour vos favoris et liens: mon site est désormais hébergé au C.N.R.S., à l’adresse….

lun. 4 nov. 013

La préparation de ma soutenance de thèse, qui aura lieu le mardi 26 novembre 2013, avance à grand pas : vous pouvez retrouver toutes les informations plus bas ou résumées dans un document qui vous indique également comment venir.

Présentation

Curriculum vitæ, English curriculum vitæ

Je suis actuellement post-doc au département Computer Science de l’Appalachian State University, sous la direction de Patricia Johann, financé par la NSF grant 1420175. J’étais auparavant dans l’équipe Spécification et vérification de systèmes du Laboratoire d’Algorithmique, Complexité et Logique (Paris 12, alias UPEC), sur contrat A.N.R. REVER, et encore avant post-doc dans l’équipe Logique De la Programmation, à l’Institut Mathématiques de Marseille (Aix-Marseille Université), sur contrat A.N.R. Ré.C.Ré.

J’ai soutenu au Laboratoire d’Informatique de Paris-Nord (Université Paris 13) le 26 novembre 2013 ma thèse en Informatique (débutée en octobre 2010 à l’école doctorale Galilée), dirigée par Stefano Guerrini et co-encadrée par Virgile Mogbil, dont le sujet est Logique linéaire et classes de complexité sous-polynomiales. J’ai auparavant effectué un Master 2 Lo.P.Hi.S.S. (désormais Lo.Phi.S.C.) à l’Université Paris 1 Panthéon-Sorbonne et un Master 2 L.M.F.I. à l’Université Paris-Diderot 7, puis un stage de 3 mois au L.I.P.N., dans l’équipe L.C.R..

Recherche

Publications et travaux

Liste des publications, Publication list, research statement

@MastersThesis{aubert2009,
  author    = {Aubert, Clément},
  school    = {Paris 1},
  title     = {L'élimination des coupures dans la Logique des Domaines Constants},
  year      = {2009},
  note      = {sous la dir. de J.-B. Joinet},
  type      = {Mémoire de M1},
  url         = {https://aubert.perso.math.cnrs.fr/recherche/memoire_m1_c_aubert.pdf},
  ids       = {memoire_m1_c_aubert}
}

@MastersThesis{aubert2010,
  author    = {Aubert, Clément},
  month     = sep,
  school    = {L.M.F.I., Paris VII},
  title     = {Réseaux de preuves booléens sous-logarithmiques},
  year      = {2010},
  note      = {sous la dir. de V. Mogbil et P. Jacobé de Naurois},
  type      = {Mémoire de M2},
  url         = {https://aubert.perso.math.cnrs.fr/recherche/stage/memoire_m2_c_aubert.pdf},
  ids         = {memoire_m2_c_aubert}
}

@Conference{aubert2011,
  author    = {Aubert, Clément},
  booktitle = {DICE 2011},
  editor      = {Marion, Jean-Yves},
  pages       = {15--27},
  series      = {Electronic Proceedings in Theoretical Computer Science},
  title       = {Sublogarithmic uniform Boolean proof nets},
  volume      = {75},
  year        = {2011},
  doi           = {10.4204/EPTCS.75.2},
  file        = {https://aubert.perso.math.cnrs.fr/recherche/sublogarithmic_uniform_boolean_proof_nets.tex},
  url           = {https://aubert.perso.math.cnrs.fr/recherche/sublogarithmic_uniform_boolean_proof_nets.pdf},
  ids           = {sublogarithmic_uniform_boolean_proof_nets}
}

@PhDThesis{aubert2013,
  author    = {Aubert, Clément},
  month     = nov,
  school    = {Université Paris 13--Sorbonne Paris Cité},
  title     = {Linear Logic and Sub-polynomial Classes of Complexity},
  year      = {2013},
  type      = {Thèse de doctorat},
  note      = {sous la dir. de S. Guerrini et V. Mogbil},
  archiveprefix = {tel},
  eprint    = {tel-00957653},
  url         = {https://aubert.perso.math.cnrs.fr/recherche/these/these_c_aubert.pdf},
  ids         = {these_c_aubert}
}

@InProceedings{aubert2014rta,
  author      = {Aubert, Clément and Bagnol, Marc},
  booktitle = {RTA-TLCA},
  editor      = {Dowek, Gilles},
  pages       = {77--92},
  publisher = {Springer},
  series      = {Lecture Notes in Computer Science},
  title       = {Unification and Logarithmic Space},
  volume      = {8650},
  year        = {2014},
  doi           = {10.1007/978-3-319-08918-8_6},
  isbn        = {978-3-319-08917-1},
  archiveprefix = {arXiv},
  eprint      = {1402.4327},
  file        = {https://aubert.perso.math.cnrs.fr/recherche/unification-and-logarithmic-space_conf.tex},
  url           = {https://aubert.perso.math.cnrs.fr/recherche/unification-and-logarithmic-space_conf.pdf},
  ids           = {unification-and-logarithmic-space_conf}
}

@InProceedings{aubert2014aplas,
  author      = {Aubert, Clément and Bagnol, Marc and Pistone, Paolo and Seiller, Thomas},
  booktitle = {APLAS},
  editor      = {Garrigue, Jacques},
  pages       = {39--57},
  publisher = {Springer},
  series      = {Lecture Notes in Computer Science},
  title       = {Logic Programming and Logarithmic Space},
  volume      = {8858},
  year        = {2014},
  doi           = {10.1007/978-3-319-12736-1_3},
  archiveprefix = {hal},
  eprint      = {hal-01309159},
  file        = {https://aubert.perso.math.cnrs.fr/recherche/logic-programming-and-logarithmic-space.tex},
  url           = {https://aubert.perso.math.cnrs.fr/recherche/logic-programming-and-logarithmic-space.pdf},
  ids           = {logic-programming-and-logarithmic-space}
}

@Article{aubert2016mscs,
  author    = {Aubert, Clément and Seiller, Thomas},
  journal   = {Mathematical Structures in Computer Science},
  month     = {may},
  pages     = {606--638},
  volume  = {26},
  issue   = {04},
  numpages= {33},
  title     = {Characterizing co-{NL} by a group action},
  year      = {2016},
  doi         = {10.1017/S0960129514000267},
  issn      = {1469-8072},
  archiveprefix = {hal},
  eprint    = {hal-01005705},
  url         = {https://aubert.perso.math.cnrs.fr/recherche/characterizing_co_nl.pdf},
  file      = {https://aubert.perso.math.cnrs.fr/recherche/characterizing_co_nl.tex},
  ids         = {characterizing_co_nl}
}

@TechReport{aubert2015inria,
  author        = {Aubert, Clément and Bagnol, Marc and Seiller, Thomas},
  type          = {Rapport de recherche},
  title         = {Memoization for Unary Logic Programming: Characterizing Ptime},
  year          = {2015},
  institution   = {{INRIA}},
  number        = {RR-8796},
  pagetotal   = {28},
  archiveprefix = {hal},
  eprint        = {hal-01107377},
  url             = {https://aubert.perso.math.cnrs.fr/recherche/Memoization_for_Unary_Logic_Programming.pdf},
  file          = {https://aubert.perso.math.cnrs.fr/recherche/Memoization_for_Unary_Logic_Programming.tex},
  ids             = {Memoization_for_Unary_Logic_Programming}
}

@Conference{aubert2015ice,
  author    = {Aubert, Clément and Cristescu, Ioana},
  booktitle = {ICE 2015},
  editor    = {Knight, Sophia and Lluch Lafuente, Alberto and Lanese, Ivan and Vieira, Hugo Torres},
  pages     = {68--95},
  series    = {Electronic Proceedings in Theoretical Computer Science},
  title     = {Reversible Barbed Congruence on Configuration Structures},
  volume    = {189},
  year      = {2015},
  doi         = {10.4204/EPTCS.189.7},
  file      = {https://aubert.perso.math.cnrs.fr/recherche/reversible_barbed_congruence_on_configuration_structures.tex},
  url         = {https://aubert.perso.math.cnrs.fr/recherche/reversible_barbed_congruence_on_configuration_structures.pdf},
  archiveprefix = {hal},
  eprint    = {hal-01157974v1},
  ids         = {reversible_barbed_congruence_on_configuration_structures}
}

@Conference{aubert2015dice,
  author    = {Aubert, Clément},
  type      = {Communication à DICE 2015},
  title     = {An in-between “implicit” and “explicit” complexity: Automata},
  year      = {2015},
  archiveprefix = {hal},
  eprint    = {hal-01111737v2},
  file      = {https://aubert.perso.math.cnrs.fr/recherche/an_in_beteen_implicit_and_explicit_complexity.tex},
  url       = {https://aubert.perso.math.cnrs.fr/recherche/an_in_beteen_implicit_and_explicit_complexity.pdf},
  ids         = {an_in_beteen_implicit_and_explicit_complexity}
}

@Unpublished{aubert2015lmcstemp,
  author      = {Aubert, Clément and Bagnol, Marc},
  pubstate  = {Soumis à Logical Methods in Computer Science, special issue of RTA/TLCA 2014},
  title       = {Unification and Logarithmic Space},
  year        = {2015},
  archiveprefix = {hal},
  eprint    = {hal-01005698},
  url           = {https://aubert.perso.math.cnrs.fr/recherche/unification-and-logarithmic-space_jour.pdf},
  file        = {https://aubert.perso.math.cnrs.fr/recherche/unification-and-logarithmic-space_jour.tex},
  ids           = {unification-and-logarithmic-space_jour}
}

@Article{aubert2017jlamp,
  author    = {Aubert, Clément and Cristescu, Ioana},
  journal   = {Journal of Logical and Algebraic Methods in Programming, special issue of ICE 2015},
  title       = {Contextual equivalences in configuration structures and reversibility},
  issn      = {2352-2208},
  year        = {2017},
  volume    = {86},
  number    = {1},
  pages     = {77--106},
  ids           = {contextual_equivalences_in_configuration_structures_and_reversibility},
  url       = {https://aubert.perso.math.cnrs.fr/recherche/contextual_equivalences_in_configuration_structures_and_reversibility.pdf},
  file      = {https://aubert.perso.math.cnrs.fr/recherche/contextual_equivalences_in_configuration_structures_and_reversibility.tex},
  archiveprefix = {hal},
  eprint    = {hal-01229408},
  doi       = {10.1016/j.jlamp.2016.08.004}
}

@InProceedings{aubert2016fossacs,
  title     = {Unary Resolution: Characterizing Ptime},
  author    = {Aubert, Clément and Bagnol, Marc and Seiller, Thomas},
  file      = {https://aubert.perso.math.cnrs.fr/recherche/Unary_Resolution_Characterizing_Ptime.tex},
  url       = {https://aubert.perso.math.cnrs.fr/recherche/Unary_Resolution_Characterizing_Ptime.pdf},
  year      = {2016},
  ids       = {Unary_Resolution_Characterizing_Ptime},
  editor    = {Jacobs, Bart and Löding, Christof},
  booktitle = {FOSSACS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  pages     = {373--389},
  doi       = {10.1007/978-3-662-49630-5_22},
  volume    = {9634},
  archiveprefix = {hal},
  eprint    = {hal-01107377},
}

@Article{aubert2016iac,
  author      = {Aubert, Clément and Seiller, Thomas},
  editor      = {Ronchi Della Rocca, Simona and Mogbil, Virgile},
  journal     = {Information and Computation},
  title       = {Logarithmic Space and Permutations},
  year        = {2016},
  volume    = {248},
  pages     = {2--21},
  url           = {https://aubert.perso.math.cnrs.fr/recherche/logarithmic_space_and_permutations.pdf},
  file        = {https://aubert.perso.math.cnrs.fr/recherche/logarithmic_space_and_permutations.tex},
  archiveprefix = {hal},
  eprint      = {hal-01005701},
  doi           = {10.1016/j.ic.2014.01.018},
  ids           = {logarithmic_space_and_permutations}
}

Exposés

Cliquer sur « En savoir plus » donne accès au résumé, aux dates et lieux des exposés. Optez pour les transparents les plus récents si le choix vous est donné. En cas de soucis techniques, désactivez le style.

Job Talks

En février 2017, j’ai donné quelques exposés dans des instituts aux USA, lors de visites aux allures d’entretiens d’embauche. Je donne quelques détails sur une autre page, me contente ici de lister ces exposés:

Reversible Barbed Congruence on Configuration Structures

(En collaboration avec Ioana Cristescu)

A standard contextual equivalence for process algebras is strong barbed congruence. Configuration structures are a denotational semantics for processes in which one can define equivalences that are more discriminating, i.e. that distinguish the denotation of terms equated by barbed congruence. Hereditary history preserving bisimulation (hhpb) is such a relation. We define a strong back and forth barbed congruence using a reversible process algebra and show that the relation induced by the back and forth congruence is equivalent to hhpb. Hence we give a characterization of hhpb as a contextual equivalence in a reversible process algebra.

An in-between “implicit” and “explicit” complexity: Automata

Implicit Computational Complexity (ICC) makes two aspects implicit, by manipulating programming languages rather than models of computation, and by internalizing the bounds rather than using external measure. We survey how automata theory contributed to complexity with a machine-dependant with implicit bounds model.

Naissance d’une approche sémantique de la complexité

La géométrie de l’interaction propose plusieurs approches pour interpréter des preuves de la logique linéaire, en se focalisant toujours sur la dynamique d’exécution. À partir de l’interprétation d’une preuve représentant un entier, il est possible de définir sémantiquement les programmes qui « interagissent bien » avec celle-ci. Ceux que J.-Y. Girard appelait « les entiers logspace » se sont révélés proposer un cadre de travail riche, capable de capturer différentes classes de complexité (L, co-NL, P). Ainsi sont nées d’autres méthodes, implicites, de faire de la complexité, et de nouveaux ponts entre théorie de la démonstration, automates, et programmation logique.

Je me propose de retracer ces 5 années de travaux menés en collaboration avec (par ordre d’apparition) Thomas Seiller, Marc Bagnol et Paolo Pistone.

  • Le 19/11/2014, à la réunion du projet A.N.R. logoi, au tableau !

La logique linéaire, outil de la théorie de la démonstration pour la complexité implicite

La logique linéaire est un système d’étude des preuves qui porte son attention sur les règles structurelles (affaiblissement, contraction) et de fait introduit dans les preuves une notion de limitation des ressources. Elle est dotée d’une dynamique de ré-écriture de preuves (l’élimination des coupures) qui est isomorphe à l’évaluation de programmes (formalisé comme la bêta-réduction dans le lambda-calcul), par la correspondance de Curry-Howard. Il est possible de n’étudier que des fragments de cette logique, et ainsi de restreindre les règles et le pouvoir expressif de ce système. Ce faisant, on peut produire des spécifications de langages de programmation à complexité bornée : tout programme rédigé dans telle syntaxe peut résoudre des problèmes d’au moins telle complexité, déterminer le résultat de l’évaluation de tel programme rédigé dans cette syntaxe nécessite au plus tant de ressources.

Ce champ de la complexité implicite fût le terrain principal de mes recherches jusqu’ici, intégrant des outils sémantiques (on interprète les preuves comme des opérateurs dans une algèbre de von Neumann, ou encore avec des termes du premier ordre) qui ont permis d’obtenir des caractérisations « abstraites » de classes de complexité célèbres (co-NL, L, P). Je vous en présenterai les grandes lignes, du cadre général de la théorie de la démonstration à la complexité implicite et même, si le temps le permets, comment les automates se sont avérés être un outil précieux et vivifiant de cette approche.

Programmation logique, unification et espace logarithmique

(En collaboration avec Marc Bagnol, Paolo Pistone et Thomas Seiller)

Nous présentons une construction algébrique qui a pour loi de composition l’unification de termes du premier ordre, et comment y représenter le calcul. La correspondance preuve-programme fournit alors une façon innovante de représenter les entiers binaires comme des fonctions dialoguant avec les programmes. Les machines abstraites que l’on peut y encoder (les observations) peuvent naturellement être vues comme des machines à pointeurs, qui parcourent l’entrée sans la modifier. On montre alors que ces observations sont suffisamment expressives pour caractériser l’espace logarithmique, et que décider de l’acceptation d’un mot par une observation est réductible au problème d’acyclicité d’un graphe, un problème également en espace logarithmique.

Quelques contributions de la Logique Linéaire à la Théorie de la complexité

En théorie de la démonstration, la Logique Linéaire propose une formalisation des preuves qui place leur dynamique au centre des investigations et porte une attention soutenue aux opérations structurelles. Depuis l’introduction des ses variantes dites bornées et allégées, la Logique Linéaire a contribué à la théorie de la complexité de différentes façons. Nous présenterons différentes avancées en nous focalisant sur les caractérisations implicites de classes de complexité, c’est-à-dire indépendantes des mesures sur des modèles abstraits. En utilisant une gamme d’outils syntaxiques et sémantiques, la Logique Linéaire est parvenu à proposer des caractérisations de l’exécution parallèle, du non-déterminisme, ou encore des programmes dit efficaces en temps ou en espace. Nous dresserons un rapide panorama de ces méthodes en les liant aux autres approches implicites de la complexité et en mettant en avant nos contributions.

Proof circuits and parallel cut-elimination in logarithmic space

Terui, Mogbil and Rahli detailed how it was possible to compute Boolean functions in parallel with proof-nets for MLLu. We introduced Proof circuits to lighten the encoding of Boolean Circuits into proof-nets, extending previous results to sub-logarithmic classes of complexity. It happened that this way of constraining our proof-nets eased their simulation by Alternating Turing Machine, the most general kind of Turing Machine. We present a small extension to previous results, where proof-nets can be normalized with logarithmic space.

Logarithmic Space and Permutations

In a recent work, Girard proposed a new and innovative approach to computational complexity based on the proofs-as-programs correspondence. The authors recently showed how Girard proposal succeeds in obtaining characterizations of L and co-NL languages as sets of operators in the hyperfinite factor of type II1. Joint work with Thomas Seiller

Linear Logic as a tool for complexity theory

Linear Logic is a formal system of deduction where proofs are ressource-sensitive. Its dynamic of proofs rewriting (cut-elimination) is naturally linked to the evaluation of programs (formalized as the beta-reduction in the Lambda calcul), thanks to the Curry-Howard correspondance. Since its introduction in 1987 by Jean-Yves Girard, it was used to characterize complexity classes, through different formalizations: Proof Nets — as a quotient on proofs inessentially differents —, rules indexed by ressource polynomials — on quantifications and modalities — or Geometry of Interaction — an even more subtle abstration of proofs – to name a few. We propose an introduction to the main concepts of Linear Logic, an overview of the methods developped to study complexity theory and conclude with the evocation of some of our characterizations through Boolean Proof Nets or Operators in a von Neuman Algebra.

On pointers, graphs, and Logspace complexity

The PURPLE programming langage developed by Hofmann and Schöpp shed a new light between classes of complexity handled by pointers and deterministic logarithmic space (L). While trying to embed it in the Geometry of Interaction framework, I met some Pointer Abstract Machines that seemed not to be used in my community, namely Kolmogorov-Uspenskii Machine (Kolmogorov and Uspenskii, 1958), Storage Modification Machines (Schönhage, 1980) and up to a certain extend One- and Two-way Finite Automata (Rabin and Scott, 1959). Those framework use graphs in different ways (as datas, working tapes or even problems), but apart from K.U.M. to S.M.M there doesn’t seem to be well-established links between them.

This short survey of those tools does not pretend to be an extensive lesson, but rather a set of open question: why don’t we use those models ? Why aren’t they refereed to ? Can they help to understand PURPLE’s relation to L?

Characterizing co-NL by a Group Action

Girard, dans Normativity in Logic (2011), propose un emploi innovant de la Géométrie de l’Interaction (GdI) dans le facteur hyperfini pour caractériser des classes de complexité. Ce papier étant très technique et parfois allusif, nous proposons avec Thomas Seiller (LAMA - Université de Savoie) une relecture des résultats qu’il présente. En allégeant et simplifiant certaines définitions et critères, en introduisant un modèle de calcul innovant (les machines à pointeurs non-déterministes), nous parvenons à prouver de nouveau que co-NL peut être caractérisé par le produit croisé du groupe des permutations finies et d’une algèbre de von Neumann.

In a recent paper, Normativity in Logic (2011), Girard uses the geometry of interaction in the hyperfinite factor in an innovative way to characterize complexity classes. As this paper is quite technical and sometimes allusive, we proposed with Thomas Seiller (Lama - Université de Savoie) a new presentation of its results. This talk will present the mathematical device that characterizes co-NL, a crossed product of the hyperfinite factor II_1 with the group of finite permutations, and the non-deterministic pointer machine, an abstract devices that computes the algorithms represented in this setting.

Proof circuits and other models of parallel computation

Proof circuits [Aubert, 11] are a clear and intuitive presentation of the Boolean proof nets [Terui, 04] in a uniform framework [Mogbil-Rahli, 07]: we define /pieces/ as a set of links and edges of a unbounded variant of Multiplicative Linear Logic representing Boolean constants, n-ary disjunctions and conjonctions, negation and mechanisms such as deletion and duplication. Thoses pieces may be “plugged” together to obtain proof circuits: MLLu uniform Boolean proof nets whose size and depth are implicitly bounded and whose parralel normalization matches up evaluation in Boolean circuits. This light presentation allows sublogarithmic translation and simulation between Boolean circuits and proof circuits, lightens the size of the latter and preserves all the good properties concerning complexity. We conclude by giving the first hints toward a full correspondence between proof circuits and alternating Turing machines, enlarging the correspondence between parallel models of computation.

Sublogarithmic uniform Boolean Proof Nets

Cut-elimination in proof nets for Multiplicative Linear Logic and evaluation in Boolean circuits may be linked using the proofs-as-programs correspondence. Those two models of parallel computation offer a framework where we can study uniformity and implicit complexity.

Boolean proof nets were introduced by [Terui, 2004] and studied by [Mogbil & Rahli, 2007] to compare the computational power of proof nets and of Boolean circuits. They established inclusions between classes of complexity that could not be extended to sublogarithmic classes as AC0 and NC1.

By restricting the way Boolean proof nets are built we prove anew those inclusion results – in an uniform framework – and extend them to small classes of complexity.

Soutenances

Cliquer sur « En savoir plus » donne accès aux dates, jury, mémoire et transparents. En cas de soucis techniques, désactivez le style.

Soutenance de thèse

Le mardi 26 novembre 2013 a eu lieu la soutenance de ma thèse, intitulée Logique linéaire et classes de complexité sous-polynomiales, devant un jury composé de

GenreNomAffiliation(qualité)
M.Patrick BaillotChargé de recherche C.N.R.S. à l’E.N.S.(rapporteur)
M.Arnaud DurandProfesseur à Denis Diderot - Paris 7(président)
MmeClaudia FaggianChargée de recherche C.N.R.S. à Denis Diderot - Paris 7
M.Stefano GuerriniProfesseur à Paris 13(directeur)
M.Ugo dal LagoRicercatore I.N.R.I.A. à l’Université de Bologne(rapporteur)
M.Jean-Yves MarionProfesseur au Lo.R.I.A. - Université de Lorraine
M.Paul-André MellièsChargé de recherche C.N.R.S. à Denis Diderot -Paris 7
M.Virgile MogbilMaître de conférence à Paris 13(co-encadrant)

Sont disponibles au téléchargement le mémoire, son errata, les transparents de la soutenance ainsi que le sujet proposé.

Soutenance de mi-parcours de thèse

Le jeudi 5 juillet 2012 j’ai effectué au L.I.P.N. une soutenance de mi-parcours en présence de

Patrick Baillot (C.N.R.S., E.N.S.) m’avait fait l’honneur d’être le rapporteur de ce travail. Vous pouvez retrouver le rapport de pré-soutenance, ainsi que les transparents de cette pré-soutenance.

Enseignement

Détail des enseignements, teaching statement, presentation of my teaching activities

Vous pouvez retrouver et ci-dessous la composition de mes enseignements (les heures y sont exprimées en heures équivalentes TP / TD) :

Vous pouvez vous référer au Programme Pédagogique National du D.U.T. R&T (pré-rentrée 2013) pour les détails des modules en IUT (dont les codes sont I3, R3, I4, AA1 et AA2).

Divers

Bourses et financements

ProgrammeInstitutRésultatDocuments
Visite de doctorant(e)GdR Informatique MathématiqueObtention d’une bourse de 420€Candidature, publication résultante du travail mené
Marie Skłodowska-Curie Individual Fellowships (IF-EF)Commission européenneScore de 83,60% (seuil : 70%), mais non financé(Bientôt?)
Research Development Travel GrantAppalachian State UniversityObtention d’une bourse de $1090Compte-rendu

Participation à des comités de programme et activité de relecture

Comité de programme :
Relecture pour journaux :
Relecture pour conférences :

Je suis également reviewer pour l’American Mathematical Society et zbMATH.

Qualifications, projets et autres affectations

Je suis qualifié dans le corps de Maître de conférence aux sections 25 (Mathématiques) et 27 (Informatique) du CNU jusqu’au 31 décembre 2019.

J’ai suis ou fus membre ou proche des projets A.N.R. suivants :

J’ai participé régulièrement aux rencontres CHoCoLa, Coquas, et fus membre du groupe de recherche interdisciplinaire Vérité et Preuves.

Écoles et séjours

Notes de cours

Ces notes ne sont en aucun cas maintenues ni vérifiées, employez-les avec précaution !

Notes manuscrites du cours de M. Pierre-Louis Curien, « Théorie de la Démonstration », donné au second semestre de l’année 2010-2011 en M2 Mathématiques à Paris 7, cursus L.M.F.I.

Notes tapuscrites du cours de M. Gabriel Sandu, « Histoire de la Logique », donné lors du premier semestre 2008-2009 en M1 Philosophie à Paris 1, cursus Lo.P.Hi.S.S.

Notes pratiques

Je regroupe dans un recoin de ce site quelques notes diverses : les outils employés pour fabriquer ce site, divers conseils pour gérer sa bibliographie avec Bib(la)tex, des liens vers quelques listes de diffusion, des notes sur les candidatures, comment accéder à un article, etc. En espérant que ça puisse être utile !