Page professionnelle de Clément Aubert

Note to English readers

My (minimal, teaching-oriented) English website is at spots.augusta.edu/caubert/. But most of the documents below are available in English and French.

Contact

Neuves

lun. 23 oct. 2023

Deux article publiés le même jour, c’est une première pour moi! Un article dans JLAMP at un article dans les actes de ATVA, les deux malheureusement derrières des paywalls, mais accessibles librement sur HAL.

Une nouvelle collaboration avec Irek Ulidowski et Iain Phillips prend forme, pour ma plus grande joie, pendant que continuent les collaborations avec le Luxembourg, la Norvège, la France, etc.

Sinon, je me bagarre avec l’administration à Augusta University pour qu’elle reconnaisse la validité d’un diplôme de l’ENS et prépare doucement le terrain pour acceuillir Deivid. Ah, et la seconde édition de SERPL était super sympa, avec ± 30 participants de 5 états (Massachusetts, Floride, Géorgie, Caroline du Nord et Pennsylvanie).

lun. 15 mai 2023

Le semestre se termine ici, et je suis ravi d’avoir

À venir:

  • deux (!) exposés à RC 2023 et un voyage en Allemagne,
  • plusieurs (!) papiers pour des journaux à finaliser / réviser,
  • des nouvelles collaborations,
  • des entretiens d’embauche pour mes postes de thèses et post-doc,
  • un dossier de tenure à rédiger (et des lettres à collecter…),
  • des projets d’été avec des étudiants,
  • etc.

mer. 1er mar. 2023

Où poster une annonce pour un contrat doctoral et une position de post-doc ? Pas facile, mais je suis bien content que le MPRI fasse des listes, ça sert dans les deux sens !

dim. 19 fév. 2023

La NSF finance désormais mon projet “Concurrency In Reversible Computations”. Un contrat doctoral et un post-doc. seront bientôt disponibles. Je fête ça avec deux soumissions à RC 2023: une seul, à propos de la réplication dans les calculs réversibles, et une avec Peter Browning, sur notre projet “Implementation of Reversible Distributed Calculus”.

Ah, et l’appel à contributions pour ICE 2023 circule, n’hésitez pas à soumettre !

jeu. 24 nov. 2022

J’ai mis à jour et trafiqué la librairie jquery que j’utilise ci-dessous pour afficher mes publications. Je code est très vilain et mal documenté, mais public.

lun. 21 nov. 2022

J’ai brièvement mis à jour ma liste de publications sur ce site. Pas un exercice passionnant, mais je suis content de

  • lister les travaux que j’ai réalisé avec Neea Rusch et nos co-auteurs Thomas Seiller et Rubiano,
  • lister les travaux que j’ai mené avec Ross Horne et Christian Johansen,
  • réaliser que la majorité de mes récentes publications (5/7) sont en libre accès (et pour le reste, il y a dissemin…).

Je ne liste pas, pour le moment, les logiciels sur lequel je travaille, mais un rapide tour sur github peut donner une idée (en attendant de Give it up Github…).

lun. 31 oct. 2022

Notre papier a été accepté à VMCAI 2023 et j’ai rejoint l’instance Mastodon hébergée par le LIPN!

lun. 11 avr. 2022

J’ai le plaisir d’avoir mon papier Concurrencies in Reversible Concurrent Calculi être accepté à la 14ème Conference on Reversible Computation, et d’avoir eu un entretien avec the International and Postdoctoral Services Office publié dans leur lettre de neuves.

lun. 31 jan. 2022

J’ai récemment reçu deux bourses d’Augusta University, et posterai sans doute les dossiers de candidature à un moment: les deux concernent les calculs reversibles et concurrents. On a aussi terminé la version longue de notre papier avec Daniele Varacca, j’ajouterai un lien dès que Hal aura accepté notre dépôt! Ah, et apparement je suis un relecteur pour le Fourth Annual Posters at the Georgia State Capitol, très bien.

lun. 29 nov. 2021

J’ai l’honneur et le plaisir d’être “ICEcreamers” (l’un des président du comité de programme) de Interaction and Concurrency Experience (ICE 2021), ainsi que membre du comité de programme de Reversible Computation (RC 2021).

mer. 13 oct. 2021

Ah ! J’organise un micro-événement à Dagstuhl !

lun. 30 aou. 2021

Je fais partie du comité de programme de Open Education Conference 2021 et ai eu le plaisir de voir notre projet pour notre cours d’introduction aux langages de programmation financé par Affordable Learning Georgia. Ce fût donc l’été des “Open Educational Ressources”!

lun. 26 avr. 2021

Notre papier Explicit Identifiers and Contexts in Reversible Concurrent Calculus avec Doriana Medić a été accepté à Reversible Computation ! Ce projet avait commencé avec l’aide de Ioana Cristescu, il est amusant de le voir porté à bien avec une autre co-auteure. Sinon, les travaux de Neea Rusch avec StATyC avancent à grands pas et on a commencé à faire circuler une première version de l’implémentation de notre analyse mwp.

sam. 26 dec. 2020

Bon, comme je le disais, il s’en est passé des choses depuis le 14 mai 2019… Entre autres,

Je tente de lister tout ça de manière comptable sur mon site, mes CV, mon paquet de tenure, mes comptes « sociaux », etc., mais ce n’est définitivement pas la partie la plus drôle de mon travail.

mer. 2 sep. 2020

Le soucis avec les sites « sur-ingeniéré » est que leur bibliothèque de dépendance croît plus vite que ma capacité à passer du temps sur ce site. Exit, donc, gulp-qui-fait-des-mises-à-jour-qui-pètent-tout, et bienvenu à un bon vieux Makefile qui ne devrait pas trop changer. Il faudra que je mette à jour le contenu, maintenant, il s’en est passé des choses depuis le 14 mai 2019…

mar. 14 mai 2019

Je viens de m’inscrire à la 11th International School on Rewriting, à laquelle il me tarde d’assister!

mer. 13 mar. 2019

Je co-organise avec Harley Eades III et Chris Martens le Southeast Regional Programming Languages Seminar à Augusta.

mar. 12 fév. 2019

Nous avons soumis avec Ioana Cristescu une version (nettement!) améliorée de History-Preserving Bisimulations on Reversible Calculus of Communicating Systems (qui est depuis devenu How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation) à FSCD 2019.

mer. 25 avr. 2018

Le semestre (et l’année) se termine ici à Augusta, et nous avons soumis avec Ioana Cristescu un article à la 10th Conference on Reversible Computation, intitulé History-Preserving Bisimulations on Reversible Calculus of Communicating Systems (qui est depuis devenu How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation). On y discute de charactérisation syntactique des relations « history-preserving », où comment la réversibilité nous enseigne des choses sur les calculs non-réversibles!

sam. 4 nov. 2017

Un poste d’Assistant professor (~maître de conférence) est ouvert au concours dans l’école où je travaile actuellement, à Augusta. Vous pouvez la retrouver sur Chronicle of Higher Education, Higher Ed. Jobs, Job ACM. N’oubliez pas, si vous souhaitez candidater à cet emploi ou à tout emploi de ce type aux États-Unis d’Amérique, de consulter ma page de conseils. Qui sait, peut-être aurez-vous besoin de mes conseils sur comment venir à Augusta?

mar. 9 oct. 2017

Voilà, j’ai désormais un site en Anglais minimal, à spots.augusta.edu/caubert/. Mon temps est pas mal croqué par les enseignements (Systèmes d’exploitation et Bases de données), mais la discussion avec Harley Eades se noue, et celle avec Ioana Cristescu se renoue.

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 Assosiate Professor (plus ou moins l’équivalent de professeur) à l’Université d’Augusta, en Géorgie, aux États-Unis d’Amérique. Précédemment, je fus en post-doctorat à l’Appalachian State University, au Laboratoire d’Algorithmique, Complexité et Logique (Paris 12, alias UPEC), et à l’Institut Mathématiques de Marseille (Aix-Marseille Université).

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. (désormais LoVe).

J’ai aussi des bio. de tailles variables, en Anglais et d’autres photos.

Recherche

Publications et travaux

Liste des publications, Publication list 

@mastersthesis{aubert2009,
    title        = {L'élimination des coupures dans la Logique des Domaines Constants},
    author       = {Aubert, Clément},
    year         = 2009,
    url          = {https://aubert.perso.math.cnrs.fr/recherche/memoire_m1_c_aubert.pdf},
    note         = {sous la dir. de J.-B. Joinet},
    school       = {Paris 1},
    type         = {Mémoire de M1}
}
@mastersthesis{aubert2010,
    title        = {Réseaux de preuves booléens sous-logarithmiques},
    author       = {Aubert, Clément},
    year         = 2010,
    month        = sep,
    url          = {https://aubert.perso.math.cnrs.fr/recherche/stage/memoire_m2_c_aubert.pdf},
    note         = {sous la dir. de V. Mogbil et P. Jacobé de Naurois},
    school       = {L.M.F.I., Paris VII},
    type         = {Mémoire de M2}
}
@conference{aubert2011,
    title        = {Sublogarithmic uniform Boolean proof nets},
    author       = {Aubert, Clément},
    year         = 2011,
    booktitle    = {DICE 2011},
    series       = {Electronic Proceedings in Theoretical Computer Science},
    volume       = 75,
    pages        = {15--27},
    doi          = {10.4204/EPTCS.75.2},
    url          = {https://aubert.perso.math.cnrs.fr/recherche/sublogarithmic_uniform_boolean_proof_nets.pdf},
    editor       = {Marion, Jean-Yves},
    file         = {https://aubert.perso.math.cnrs.fr/recherche/sublogarithmic_uniform_boolean_proof_nets.tex}
}
@phdthesis{aubert2013,
    title        = {Linear Logic and Sub-polynomial Classes of Complexity},
    author       = {Aubert, Clément},
    year         = 2013,
    month        = nov,
    url          = {https://aubert.perso.math.cnrs.fr/recherche/these/these_c_aubert.pdf},
    note         = {sous la dir. de S. Guerrini et V. Mogbil},
    school       = {Université Paris 13--Sorbonne Paris Cité},
    type         = {Thèse de doctorat},
    archiveprefix = {tel},
    eprint       = {tel-00957653}
}
@inproceedings{aubert2014rta,
    title        = {Unification and Logarithmic Space},
    author       = {Aubert, Clément and Bagnol, Marc},
    year         = 2014,
    booktitle    = {RTA-TLCA 2014},
    publisher    = {Springer},
    series       = {Lecture Notes in Computer Science},
    volume       = 8650,
    pages        = {77--92},
    doi          = {10.1007/978-3-319-08918-8_6},
    isbn         = {978-3-319-08917-1},
    url          = {https://aubert.perso.math.cnrs.fr/recherche/unification-and-logarithmic-space_conf.pdf},
    editor       = {Dowek, Gilles},
    archiveprefix = {arXiv},
    eprint       = {1402.4327},
    file         = {https://aubert.perso.math.cnrs.fr/recherche/unification-and-logarithmic-space_conf.tex}
}
@inproceedings{aubert2014aplas,
    title        = {Logic Programming and Logarithmic Space},
    author       = {Aubert, Clément and Bagnol, Marc and Pistone, Paolo and Seiller, Thomas},
    year         = 2014,
    booktitle    = {APLAS 2014},
    publisher    = {Springer},
    series       = {Lecture Notes in Computer Science},
    volume       = 8858,
    pages        = {39--57},
    doi          = {10.1007/978-3-319-12736-1_3},
    url          = {https://aubert.perso.math.cnrs.fr/recherche/logic-programming-and-logarithmic-space.pdf},
    editor       = {Garrigue, Jacques},
    archiveprefix = {hal},
    eprint       = {hal-01309159},
    file         = {https://aubert.perso.math.cnrs.fr/recherche/logic-programming-and-logarithmic-space.tex}
}
@article{aubert2016mscs,
    title        = {Characterizing co-{NL} by a group action},
    author       = {Aubert, Clément and Seiller, Thomas},
    year         = 2016,
    month        = may,
    journal      = {Mathematical Structures in Computer Science},
    volume       = 26,
    pages        = {606--638},
    doi          = {10.1017/S0960129514000267},
    issn         = {1469-8072},
    url          = {https://aubert.perso.math.cnrs.fr/recherche/characterizing_co_nl.pdf},
    issue        = {04},
    numpages     = 33,
    archiveprefix = {hal},
    eprint       = {hal-01005705},
    file         = {https://aubert.perso.math.cnrs.fr/recherche/characterizing_co_nl.tex}
}
@techreport{aubert2015inria,
    title        = {Memoization for Unary Logic Programming: Characterizing Ptime},
    author       = {Aubert, Clément and Bagnol, Marc and Seiller, Thomas},
    year         = 2015,
    number       = {RR-8796},
    url          = {https://aubert.perso.math.cnrs.fr/recherche/Memoization_for_Unary_Logic_Programming.pdf},
    type         = {Rapport de recherche},
    institution  = {{INRIA}},
    pagetotal    = 28,
    archiveprefix = {hal},
    eprint       = {hal-01107377},
    file         = {https://aubert.perso.math.cnrs.fr/recherche/Memoization_for_Unary_Logic_Programming.tex}
}
@conference{aubert2015ice,
    title        = {Reversible Barbed Congruence on Configuration Structures},
    author       = {Aubert, Clément and Cristescu, Ioana},
    year         = 2015,
    booktitle    = {ICE 2015},
    series       = {Electronic Proceedings in Theoretical Computer Science},
    volume       = 189,
    pages        = {68--95},
    doi          = {10.4204/EPTCS.189.7},
    url          = {https://aubert.perso.math.cnrs.fr/recherche/reversible_barbed_congruence_on_configuration_structures.pdf},
    editor       = {Knight, Sophia and Lluch Lafuente, Alberto and Lanese, Ivan and Vieira, Hugo Torres},
    file         = {https://aubert.perso.math.cnrs.fr/recherche/reversible_barbed_congruence_on_configuration_structures.tex},
    archiveprefix = {hal},
    eprint       = {hal-01157974v1}
}
@conference{aubert2015dice,
    title        = {An in-between “implicit” and “explicit” complexity: Automata},
    author       = {Aubert, Clément},
    year         = 2015,
    booktitle    = {DICE 2015},
    url          = {https://aubert.perso.math.cnrs.fr/recherche/an_in_beteen_implicit_and_explicit_complexity.pdf},
    institution  = {LACL},
    archiveprefix = {hal},
    eprint       = {hal-01111737v2},
    file         = {https://aubert.perso.math.cnrs.fr/recherche/an_in_beteen_implicit_and_explicit_complexity.tex}
}
@article{Aubert2018lmcs,
    title        = {Unification and Logarithmic Space},
    author       = {Aubert, Clément and Bagnol, Marc},
    year         = 2018,
    journal      = {Logical Methods in Computer Science},
    volume       = 14,
    number       = 3,
    doi          = {10.23638/LMCS-14(3:6)2018},
    url          = {https://aubert.perso.math.cnrs.fr/recherche/unification-and-logarithmic-space_jour.pdf},
    archiveprefix = {hal},
    eprint       = {hal-01157984},
    file         = {https://aubert.perso.math.cnrs.fr/recherche/unification-and-logarithmic-space_jour.tex}
}
@article{aubert2017jlamp,
    title        = {Contextual equivalences in configuration structures and reversibility},
    author       = {Aubert, Clément and Cristescu, Ioana},
    year         = 2017,
    journal      = {Journal of Logical and Algebraic Methods in Programming},
    volume       = 86,
    number       = 1,
    pages        = {77--106},
    doi          = {10.1016/j.jlamp.2016.08.004},
    issn         = {2352-2208},
    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}
}
@inproceedings{aubert2016fossacs,
    title        = {Unary Resolution: Characterizing Ptime},
    author       = {Aubert, Clément and Bagnol, Marc and Seiller, Thomas},
    year         = 2016,
    booktitle    = {FOSSACS 2016},
    publisher    = {Springer},
    series       = {Lecture Notes in Computer Science},
    volume       = 9634,
    pages        = {373--389},
    doi          = {10.1007/978-3-662-49630-5_22},
    url          = {https://aubert.perso.math.cnrs.fr/recherche/Unary_Resolution_Characterizing_Ptime.pdf},
    file         = {https://aubert.perso.math.cnrs.fr/recherche/Unary_Resolution_Characterizing_Ptime.tex},
    editor       = {Jacobs, Bart and Löding, Christof},
    archiveprefix = {hal},
    eprint       = {hal-01107377}
}
@article{aubert2016iac,
    title        = {Logarithmic Space and Permutations},
    author       = {Aubert, Clément and Seiller, Thomas},
    year         = 2016,
    journal      = {Information and Computation},
    volume       = 248,
    pages        = {2--21},
    doi          = {10.1016/j.ic.2014.01.018},
    url          = {https://aubert.perso.math.cnrs.fr/recherche/logarithmic_space_and_permutations.pdf},
    editor       = {Ronchi Della Rocca, Simona and Mogbil, Virgile},
    file         = {https://aubert.perso.math.cnrs.fr/recherche/logarithmic_space_and_permutations.tex},
    archiveprefix = {hal},
    eprint       = {hal-01005701}
}
@techreport{aubert2019category,
    title        = {Categories for Me, and You?},
    author       = {Aubert, Clément},
    year         = 2019,
    number       = {},
    url          = {https://aubert.perso.math.cnrs.fr/recherche/categories_for_me.pdf},
    type         = {Rapport de recherche},
    institution  = {Augusta University},
    pagetotal    = 45,
    archiveprefix = {hal},
    eprint       = {hal-02308858},
    file         = {https://aubert.perso.math.cnrs.fr/recherche/categories_for_me.zip}
}
@conference{aubert2020ice,
    title        = {Structural Equivalence in Reversible Calculus of Communicating Systems (Abstract)},
    author       = {Aubert, Clément and Cristescu, Ioana},
    year         = 2020,
    booktitle    = {ICE 2020},
    url          = {https://aubert.perso.math.cnrs.fr/recherche/structural_equivalence_in_rccs_abstract.pdf},
    archiveprefix = {hal},
    eprint       = {hal-02118036},
    file         = {https://aubert.perso.math.cnrs.fr/recherche/structural_equivalence_in_rccs_abstract.tex}
}
@inproceedings{Aubert2020concur,
    title        = {How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation},
    author       = {Aubert, Clément and Cristescu, Ioana},
    year         = 2020,
    booktitle    = {CONCUR 2022},
    publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
    series       = {LIPIcs},
    volume       = 2017,
    pages        = {7:1--7:23},
    doi          = {10.4230/LIPIcs.CONCUR.2020.7},
    url          = {https://aubert.perso.math.cnrs.fr/recherche/how_reversibility_can_solve_traditional_questions.pdf},
    editor       = {Igor Konnov and Laura Kovács},
    file         = {https://aubert.perso.math.cnrs.fr/recherche/how_reversibility_can_solve_traditional_questions.tex}
}
@conference{Aubert2020Process,
    title        = {{Process, Systems and Tests: Three Layers in Concurrent Computation}},
    author       = {Aubert, Clément and Varacca, Daniele},
    year         = 2021,
    booktitle    = {Proceedings 14th Interaction and Concurrency Experience, {ICE} 2021, Online, 18th June 2021},
    series       = {{EPTCS}},
    volume       = 347,
    pages        = {1--21},
    doi          = {10.4204/EPTCS.347.1},
    url          = {https://aubert.perso.math.cnrs.fr/recherche/process_systems_tests.pdf},
    file         = {https://aubert.perso.math.cnrs.fr/recherche/process_systems_tests.tex},
    editor       = {Lange, Julien and Mavridou, Anastasia and Safina, Larisa and Scalas,  Alceste}
}
@article{Aubert2022jlamp,
    title        = {Processes Against Tests: On Defining Contextual Equivalences},
    author       = {Aubert, Clément and Varacca, Daniele},
    year         = 2022,
    journal      = {Journal of Logical and Algebraic Methods in Programming},
    pages        = 100799,
    doi          = {10.1016/j.jlamp.2022.100799},
    issn         = {2352-2208},
    archiveprefix = {hal},
    eprint       = {hal-03535565}
}
@inproceedings{Aubert2021RC,
    title        = {Explicit Identifiers and Contexts in Reversible Concurrent Calculus},
    author       = {Aubert, Clément and Medić,  Doriana},
    year         = 2021,
    booktitle    = {RC 2021},
    publisher    = {Springer},
    series       = {Lecture Notes in Computer Sciences},
    volume       = 12805,
    pages        = {144--162},
    doi          = {10.1007/978-3-030-79837-6_9},
    editor       = {Yamashita, Shigeru and Yokoyama, Tetsuo},
    archiveprefix = {hal},
    eprint       = {hal-03183053v1}
}
@proceedings{ICE2022,
    title        = {Proceedings 15th Interaction and Concurrency Experience, {ICE} 2022, Lucca, Italy, 17th June 2022},
    year         = 2022,
    publisher    = {Open Publishing Association},
    series       = {EPTCS},
    volume       = 365,
    doi          = {10.4204/EPTCS.365},
    editor       = {Aubert, Clément and Di Giusto, Cinzia and Safina, Larisa and Scalas, Alceste}
}
@proceedings{ICE2023,
    title        = {Proceedings 16th Interaction and Concurrency Experience, {ICE} 2023, Lisbon, Portugal, 19th June 2023},
    year         = 2023,
    publisher    = {Open Publishing Association},
    series       = {EPTCS},
    volume       = 383,
    doi          = {10.4204/EPTCS.383},
    editor       = {Clément Aubert and Cinzia Di Giusto and Simon Fowler and Larisa Safina}
}
@inproceedings{Aubert2022ExpressSos,
    title        = {Bisimulations Respecting Duration and Causality for the Non-interleaving Applied π-Calculus},
    author       = {Aubert, Clément and Horne, Ross and Johansen, Christian},
    year         = 2022,
    booktitle    = {EXPRESS/SOS 2022},
    series       = {{EPTCS}},
    volume       = 368,
    pages        = {3--22},
    doi          = {10.4204/EPTCS.368.1},
    editor       = {Castiglioni, Valentina and Mezzina, Claudio Antares}
}
@inproceedings{Aubert2022Concur,
    title        = {Diamonds for Security: {A} Non-Interleaving Operational Semantics for the Applied Pi-Calculus},
    author       = {Aubert, Clément and Horne, Ross and Johansen, Christian},
    year         = 2022,
    booktitle    = {CONCUR 2022},
    publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
    series       = {LIPIcs},
    volume       = 243,
    pages        = {30:1--30:26},
    doi          = {10.4230/LIPIcs.CONCUR.2022.30},
    editor       = {Klin, Bartek and Lasota, Slawomir and Muscholl, Anca}
}
@inproceedings{Aubert2022RC,
    title        = {Concurrencies in Reversible Concurrent Calculi},
    author       = {Aubert, Clément},
    year         = 2022,
    booktitle    = {RC 2022},
    publisher    = {Springer},
    series       = {Lecture Notes in Computer Science},
    volume       = 13354,
    pages        = {146--163},
    doi          = {10.1007/978-3-031-09005-9\_10},
    editor       = {Mezzina, Claudio Antares and Podlaski, Krzysztof},
    archiveprefix = {hal},
    eprint       = {hal-03605003}
}
@inproceedings{Aubert2022FSCD,
    title        = {mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity},
    author       = {Aubert, Clément and Rubiano, Thomas and Rusch, Neea and Seiller, Thomas},
    year         = 2022,
    booktitle    = {FSCD 2022},
    publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
    series       = {LIPIcs},
    volume       = 228,
    pages        = {26:1--26:23},
    doi          = {10.4230/LIPIcs.FSCD.2022.26},
    editor       = {Felty, Amy P.}
}
@inproceedings{Aubert2022CRIS,
    title        = {Data Integration for the Study of Outstanding Productivity in Biomedical Research},
    author       = {Aubert, Clément and Balas, E Andrew and Townsend, Tiffany and Sleeper, Noah and Tran, CJ},
    year         = 2022,
    booktitle    = {CRIS 2022},
    publisher    = {Elsevier},
    series       = {Procedia Computer Science},
    volume       = 211,
    pages        = {196--200},
    doi          = {10.1016/j.procs.2022.10.191},
    issn         = {1877-0509},
    editor       = {Sicilia, Miguel-Angel and De-Castro, Pablo and Vancauwenbergh, Sadia and Simons, Ed and Ognjen, Orel},
    archiveprefix = {handle},
    eprint       = {11366/1987}
}
@conference{Aubert2022Types,
    title        = {Realizing Implicit Computational Complexity},
    author       = {Aubert, Clément and Rubiano, Thomas and Rusch, Neea and Seiller, Thomas},
    year         = 2022,
    month        = Mar,
    booktitle    = {Types 2022},
    editor       = {Kesner, Delia and Pédrot, Pierre-Marie},
    archiveprefix = {hal},
    eprint       = {hal-03603510}
}
@inproceedings{AubertRRS23,
    title        = {Distributing and Parallelizing Non-canonical Loops},
    author       = {Aubert, Clément and Rubiano, Thomas and Rusch, Neea and Seiller, Thomas},
    year         = 2023,
    booktitle    = {{VMCAI} 2023},
    publisher    = {Springer},
    series       = {Lecture Notes in Computer Science},
    volume       = 13881,
    pages        = {1--24},
    doi          = {10.1007/978-3-031-24950-1\_1},
    editor       = {Dragoi, Cezara and Emmi, Michael and Wang, Jingbo}
}
@inproceedings{AubertRRC23,
    title        = {Replications in Reversible Concurrent Calculi},
    author       = {Clément Aubert},
    year         = 2023,
    booktitle    = {{RC} 2023},
    publisher    = {Springer},
    series       = {Lecture Notes in Computer Science},
    volume       = 13960,
    pages        = {15--23},
    doi          = {10.1007/978-3-031-38100-3_2},
    editor       = {Martin Kutrib and Uwe Meyer},
    archiveprefix = {hal},
    eprint       = {hal-04174437}
}
@inproceedings{AubertIRDC23,
    title        = {Implementation of a Reversible Distributed Calculus},
    author       = {Clément Aubert and Peter Browning},
    year         = 2023,
    booktitle    = {{RC} 2023},
    publisher    = {Springer},
    series       = {Lecture Notes in Computer Science},
    volume       = 13960,
    pages        = {210--217},
    doi          = {10.1007/978-3-031-38100-3_13},
    editor       = {Martin Kutrib and Uwe Meyer},
    archiveprefix = {hal},
    eprint       = {hal-04174439}
}
@article{AubertRCC23,
    title        = {The Correctness of Concurrencies in (Reversible) Concurrent Calculi},
    author       = {Clément Aubert},
    year         = 2023,
    journal      = {Journal of Logical and Algebraic Methods in Programming},
    pages        = 100924,
    doi          = {10.1016/j.jlamp.2023.100924},
    issn         = {2352-2208},
    archiveprefix = {hal},
    eprint       = {hal-03950347}
}
@inproceedings{AubertPymwp23,
    title        = {pymwp: A Static Analyzer Determining Polynomial Growth Bounds},
    author       = {Aubert, Clément and Rubiano, Thomas and Rusch, Neea and Seiller, Thomas},
    year         = 2023,
    booktitle    = {{ATVA} 2023},
    publisher    = {Springer Nature Switzerland},
    address      = {Cham},
    doi          = {10.1007/978-3-031-45332-8_14},
    pages        = {263--275},
    isbn         = {978-3-031-45332-8},
    editor       = {André, Étienne and Sun, Jun},
    archiveprefix = {hal},
    eprint       = {hal-03269121}
}

Exposés

Cliquer sur « En savoir plus » donne accès au résumé, aux dates et lieux des exposés. En cas de soucis techniques, désactivez le style.

Applying Implicit Computational Complexity

This presentation is interested in reasoning about the recent development of static analyzers and optimizers inspired by Implicit Computational Complexity (ICC), which illustrate the challenges and benefits of applying approaches stemming from proof theory to software development.

Résumé complet sur le site de la réunion

Reversing your Computation, but Why?

A typical computer user knows the difference between what can be undone on a computer, and what cannot. They may be familiar with the “undo” feature of text editors but understand the impossibility of recovering an unsaved document after an emergency shutdown. Creating programs guaranteeing that any action can be undone requires to design and implement reversible programming languages. While such languages come with interesting built-in security features (because any past action can be investigated), they also raise challenges when it comes to concurrency. Indeed, undoing an action that involved synchronization between multiple actors requires all actors to agree to undo said action. This talk offers to discuss current trends in solving the aforementioned problem, and to highlight some of the benefits that could result from well-designed concurrent and reversible programming languages.

A Brief Overview of Process Calculi

This presentation is a gentle introduction to process calculus, which is a formal method for concurrent systems. I will briefly present Robin Milner’s seminal work on the Calculus of Communicating Systems (CCS) and how, through successive enrichments and refined study, it led to the development of certified network protocols and implementations.

  • Exposé donné au SCCS Research Colloquium, à Augusta University, le 16 Février 2024: transparents

Replications in Reversible Concurrent Calculi

Process calculi such as CCS or the π-calculus provide specification languages for the study and correctness of communication protocols. They also served in detailing subtle differences between formalisms to represent infinite behaviors, notably in expressiveness. To our knowledge, such results were never investigated from a reversible perspective. One question we would like to answer is how recursion, replication and iteration compare in the reversible setting. Of course, comparing them requires to define them first, and this short note draws possible paths toward a definition of replication for reversible concurrent calculi.

The Correctness of Concurrencies in (Reversible) Concurrent Calculi

Most computers today are designed to operate unidirectionally, but adiabatic, quantum, and biological computers require bidirectional flow of computation, as they are reversible in nature. Those promising technologies have already started to revolutionize the very essence of computing, but also of communicating. Of interest to us are specification languages for reversible protocols, and how they can enlighten our understanding of what it means to “undo” a communication. The work we will be presenting is concerned with operator algebras, and more particularly with the notion(s) of independence (or concurrency) they use. We will present a novel correctness criterion for the definition of concurrency for reversible systems, that can in retrospect provide forward-only systems a way of checking that their definitions of independence for co-initial and composable transitions “play well together”.

This work is an extension of a recent publication in Reversible Computation 2022, whose submitted pre-print is available at https://hal.science/hal-03950347v1.

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

Genre Nom Affiliation (qualité)
M. Patrick Baillot Chargé de recherche C.N.R.S. à l’E.N.S. (rapporteur)
M. Arnaud Durand Professeur à Denis Diderot - Paris 7 (président)
Mme Claudia Faggian Chargée de recherche C.N.R.S. à Denis Diderot - Paris 7  
M. Stefano Guerrini Professeur à Paris 13 (directeur)
M. Ugo dal Lago Ricercatore I.N.R.I.A. à l’Université de Bologne (rapporteur)
M. Jean-Yves Marion Professeur au Lo.R.I.A. - Université de Lorraine  
M. Paul-André Melliès Chargé de recherche C.N.R.S. à Denis Diderot - Paris 7  
M. Virgile Mogbil Maî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

Pour les enseignements effectués à l’Université d’Augusta, se référer à spots.augusta.edu/caubert/. Vous pouvez retrouver ci-dessous la composition de mes enseignements pré-2017 (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

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 !

Bourses et financements

Programme Institut Résultat Documents
Visite de doctorant(e) GdR Informatique Mathématique Financé – 420€ Candidature, publication résultante du travail mené
Marie Skłodowska-Curie Individual Fellowships (IF-EF) Commission européenne Score de 83,60% (seuil : 70%), mais non financé Projet proposé, Evaluation Summary Report
Research Development Travel Grant Appalachian State University Financé – $1 090 Projet Proposé, Compte-rendu
Mini-Grant for Ancillary Materials Creation and Revision Affordable Learning Georgia Financé – $2 800 Site du projet
Summer Scholars Program Center for Undergraduate Research & Scholarship Financé – $3 600 Site du projet
Transatlantic Research Partnership FACE Foundation Financé – $20 000 Site du projet
Affordable Materials Grants Affordable Learning Georgia Financé – $30 000 Site du projet
Research Scholarship Creative Activity Augusta University’s Sponsored Programs Administration Financé – $10 000 -
Summer Scholars Program Center for Undergraduate Research & Scholarship Financé – $3 660 Site du projet
NSF Core Program NSF Financé – $582 562 Site du projet

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

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

Je suis également reviewer pour l’American Mathematical Society et zbMATH. L’ensemble de mes reviews peut être consulté librement sur le site de l’AMS et sur le site de zbMATH.

Qualifications, projets et autres affectations

Je fus 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.

Je 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 ont été prises lorsque j’étais moi-même étudiant. Elles ne sont pas maintenues, 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.