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.
My (minimal, teaching-oriented) English website is at spots.augusta.edu/caubert/. But most of the documents below are available in English and French.
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).
Le semestre se termine ici, et je suis ravi d’avoir
À venir:
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 !
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 !
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.
J’ai brièvement mis à jour ma liste de publications sur ce site. Pas un exercice passionnant, mais je suis content de
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…).
Notre papier a été accepté à VMCAI 2023 et j’ai rejoint l’instance Mastodon hébergée par le LIPN!
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.
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.
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).
Ah ! J’organise un micro-événement à Dagstuhl !
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”!
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.
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.
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…
Je viens de m’inscrire à la 11th International School on Rewriting, à laquelle il me tarde d’assister!
Je co-organise avec Harley Eades III et Chris Martens le Southeast Regional Programming Languages Seminar à Augusta.
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.
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!
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?
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.
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!
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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).
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.
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.
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.
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).
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.
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.
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.
D’aucuns cherchent à tout prix à avoir un CDI d’enseignant-chercheur, d’autres alertent en démissionnant… (archive).
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.
Notre article Logic Programming and Logarithmic Space a été accepté à APLAS. Super, je peux mettre à jour mon c.v..
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).
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.
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.
Notre article Unification and Logarithmic Space, avec Marc Bagnol, a été accepté à RTA/TLCA 2014.
Je mets en ligne quelques notes concernant les listes de di(ffu|scus)sion dans mon domaine.
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.
Veuillez mettre à jour vos favoris et liens: mon site est désormais hébergé au C.N.R.S., à l’adresse….
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.
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.
Liste des publications, Publication list
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.
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
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.
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.
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.
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.
Vous pouvez retrouver ce travail présenté dans cet article.
(En collaboration avec Ioana Cristescu)
Vous pouvez retrouver ce travail présenté dans cet article.
(En collaboration avec Daniele Varacca)
Voir le cours résumé de ce travail en cours.
(En collaboration avec Ioana Cristescu)
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:
(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.
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.
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.
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.
(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.
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.
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.
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 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.
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?
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 [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.
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.
Cliquer sur « En savoir plus » donne accès aux dates, jury, mémoire et transparents. En cas de soucis techniques, désactivez le style.
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é.
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.
Mon mémoire de M2, Réseaux de preuves booléens, a été soutenu le 23 septembre 2010 devant un jury composé d’Arnaud Durand, de Paul Rozière et mes deux directeurs, Virgile Mogbil et Paulin Jacobé de Naurois.
Sont disponibles au téléchargement le mémoire, les transparents ainsi que le sujet.
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).
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 !
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.
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.
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.