Retrouver une information et comprendre sa portée.
Ces relevés documentaires complètent la préparation d’un projet. Choisissez le référentiel adapté à votre question, puis ouvrez la fiche et sa source pour vérifier le périmètre et le millésime.
Choisir le bon point de départ
Quelle information cherchez-vous ?
Les données sont des copies locales de sources identifiées, pas une consultation en temps réel. Une absence dans le relevé ne prouve pas une absence dans la source.
Compétences
Métiers et formations
Un métier décrit des activités ; une certification atteste un cadre de compétences ; une formation prépare un parcours. Comparez ces objets séparément.
Une adresse administrative ne constitue pas une zone de service. Une présence d’équipement ne mesure ni le stock, ni l’accueil, ni la qualité d’une prestation.
Choisissez un référentiel et affinez la recherche. Les fiches précisent la source, le millésime et les limites des informations publiées.
Distinguer publication et disponibilité du texte
Une notice signale un travail et ses métadonnées ; le résumé ne remplace pas les méthodes et résultats du texte intégral. Vérifiez le type de document et la version accessible avant de citer une conclusion. La présence dans une archive ouverte ne démontre pas à elle seule l’évaluation par les pairs ni l’applicabilité à votre situation.
Explorer les entrées et leurs sources
Les résultats proviennent des relevés indiqués ci-dessous. La zone sélectionnée s’applique aux statistiques et aux lieux, tandis que les aliments, produits, métiers, fiches pratiques, activités, notions, certifications et bibliographies restent des référentiels nationaux. Les travaux de recherche couvrent des références nationales ou internationales.
442 résultats · page 1 sur 25 · jusqu’à 18 entrées affichées. Classement par année décroissante puis titre.
Explorer les revues et périodiques — 70 fiches HAL liées
Revues, périodiques et travaux associés
Rechercher un titre, une abréviation, un ISSN ou un éditeur renseigné, puis lire les références HAL associées à une fiche précise. Le répertoire couvre 86 notices liées dans la sélection du site, avant les autres filtres de recherche.
70 fiche(s) correspondant à la recherche · page 1 sur 4.
Revues et périodiques liés aux références retenues — ordre alphabétique
Source : HAL et son référentiel des revues, CCSD. Complément de métadonnées relevé le 23 octobre 2026, associé aux références documentaires du 22 octobre 2026. Les métadonnées sont réutilisables sous CC0 ; les droits des textes intégraux restent propres à chaque document.
Seules les références portant un titre de revue dans le relevé initial sont interrogées. L’identifiant numérique du document, son identifiant HAL, sa version et son titre de revue doivent correspondre avant d’utiliser son identifiant de revue. La fiche cible doit être récupérée dans le référentiel. Un identifiant direct est privilégié ; une correspondance d’ancien identifiant n’est utilisable que si elle est explicitement publiée et univoque. Une référence non confirmée conserve ses informations d’origine, sans lien ajouté.
Les homonymes restent séparés par leurs identifiants. Ni le titre seul, ni un ISSN, ni le nom d’un éditeur ne servent à fusionner les fiches. L’absence de champ ne prouve pas l’absence d’éditeur ou d’identifiant. Les statuts techniques de HAL ne constituent pas une appréciation scientifique.
Les nombres portent sur les notices de la sélection du site, pas sur l’ensemble du contenu d’une revue. Des notices différentes peuvent décrire un même travail. Aucun facteur d’impact, nombre de citations, classement, tarif ou disponibilité n’est déduit. Les conditions actuelles d’accès, d’abonnement et de dépôt restent à vérifier auprès du périodique et sur la notice HAL.
Explorer les disciplines — 142 domaines HAL dans cette sélection
Choisissez un domaine pour consulter les notices dont le code est publié dans HAL. Les effectifs portent sur toute la sélection du site, avant les autres filtres ; un identifiant HAL est compté une seule fois par domaine. Une notice peut figurer dans plusieurs domaines : les effectifs ne s’additionnent pas.
Chimie (chim) — 2 notices, dont 1 avec ce domaine principal.
Chimie/Catalyse (chim.cata) — 3 notices, dont 2 avec ce domaine principal.
Libellés et codes du référentiel des domaines HAL, relevés le 23 octobre 2026. Le regroupement utilise les codes effectivement publiés dans les notices ; aucun rattachement supplémentaire n’est déduit des intitulés.
Colloques, congrès et rencontres cités — 113 intitulés dans cette sélection
Ces intitulés sont ceux publiés dans les notices HAL retenues par le site. Un intitulé identique peut couvrir plusieurs éditions ; les dates restent celles de chaque notice. Les variations d’écriture restent séparées. Les effectifs comptent une fois chaque identifiant HAL, avant les autres filtres.
Source : métadonnées HAL / CCSD, relevées le 23 octobre 2026. Ce répertoire décrit les travaux déposés ; il ne constitue pas un agenda d’inscription aux événements.
Lire des références de recherche sur logiciels, web et conception numérique. Les axes ci-dessous organisent cette sélection documentaire ; ils ne constituent pas une évaluation critique des travaux. Les références sont nationales ou internationales ; le choix d’un territoire ne filtre pas cette bibliographie. Rechercher un titre, un auteur, des mots-clés, un identifiant HAL ou un DOI.
Notices HAL — métadonnées récupérées le 22 octobre 2026
Source : HAL, archive ouverte développée par le Centre pour la communication scientifique directe (CCSD). Métadonnées bibliographiques initiales récupérées le 22 octobre 2026, réutilisées sous CC0 1.0. Les droits du document lui-même sont précisés sur sa notice officielle.
Cette sélection retient au plus les 200 premiers résultats par recherche sur les titres et mots-clés de HAL, triés par date du travail décroissante, pour les années 2000 à 2026. Les titres et mots-clés sont contrôlés à nouveau pour les termes de chaque axe. Un identifiant HAL est compté une seule fois par site ; la version la plus élevée rencontrée dans les réponses retenues est conservée. Des notices différentes peuvent encore décrire un même travail. La sélection n’est pas exhaustive et son ordre ne constitue pas un classement de qualité.
Articles, communications, thèses, mémoires, rapports et prépublications ont des statuts documentaires distincts. Le dépôt dans une archive et le type indiqué ne suffisent pas à établir une évaluation par les pairs. Les résumés sont ceux fournis dans les métadonnées, attribués aux auteurs de la notice ; ils restent à lire avec le travail complet et son contexte. Leur présence ne vaut pas recommandation médicale, juridique, financière ou technique.
La date du travail, la date de dépôt et la date de modification décrivent des événements différents. Un fichier signalé dans HAL ne garantit pas son accès actuel ; la notice officielle précise les conditions de consultation. Les axes sont documentaires : ils ne localisent pas les auteurs ni les terrains d’étude dans le territoire sélectionné ailleurs sur la page.
Oui — déclaré disponible en libre accès sur HAL ou sur un autre serveur
Type de dépôt publié dans ce relevé
file
Licence du document publiée dans ce relevé
https://about.hal.science/hal-authorisation-v1/
Les liens et l’indicateur décrivent le relevé de métadonnées ; les conditions d’accès peuvent évoluer. Une annexe ou une ressource liée peut avoir des conditions distinctes de celles du fichier principal. La licence affichée reste celle déclarée dans la notice. Source : notice officielle HAL, version 1, identifiant de document 3560564. Définition des champs de l’API HAL ; métadonnées HAL sous CC0.
Structures de recherche indexées dans HAL — 9 fiches reliées
Structures indexées dans la notice HAL tel-03560564, version 1. Relevé et référentiel consultés le 23 octobre 2026. Cette indexation peut inclure des structures parentes ; elle n’attribue pas chacune de ces structures à chaque auteur.
Structures identifiées dans le référentiel HAL — laboratoires, équipes et établissements conservés séparément
Les statuts VALID, OLD et INCOMING décrivent le traitement des fiches dans le référentiel. Les dates, adresses et identifiants ne permettent pas de déduire l’activité actuelle d’un organisme ni l’affiliation actuelle d’un auteur. Les codes pays concernent les structures, pas les terrains d’étude.
Autres notices indexées avec Centre Inria de Saclay
8 autre(s) notice(s) dans la sélection du site, avant les filtres de recherche.
Jusqu’à six notices sont affichées par année du travail décroissante. Une structure commune ne prouve pas une collaboration entre les auteurs. Ces nombres décrivent la sélection du site et non la production complète de la structure.
Autres notices indexées avec Centre Inria de l'Université Paris-Saclay
8 autre(s) notice(s) dans la sélection du site, avant les filtres de recherche.
Jusqu’à six notices sont affichées par année du travail décroissante. Une structure commune ne prouve pas une collaboration entre les auteurs. Ces nombres décrivent la sélection du site et non la production complète de la structure.
Autres notices indexées avec CentraleSupélec
40 autre(s) notice(s) dans la sélection du site, avant les filtres de recherche.
Jusqu’à six notices sont affichées par année du travail décroissante. Une structure commune ne prouve pas une collaboration entre les auteurs. Ces nombres décrivent la sélection du site et non la production complète de la structure.
Ce classement décrit l’indexation documentaire du dépôt. Il ne constitue ni un label de qualité, ni une spécialité professionnelle attribuée aux auteurs. Les liens vers d’autres travaux reposent sur un code commun dans les métadonnées et affichent au plus six notices par domaine, par année du travail décroissante. La hiérarchie ci-dessus reprend les identifiants parents du référentiel ; elle ne modifie pas les codes du dépôt.
Auteurs indexés : Quentin Garchery. Source : tel-03560564, version 1.
De nombreux prouveurs et outils de vérification font un usage instensif des transformations logiques afin de ramener un problème exprimé sous la forme d'une tâche de preuve à un certain nombre de tâches de preuve plus simples à valider. Les transformations font souvent partie de la base de confiance de l'outil de vérification. Cette thèse a pour objectif de renforcer la confiance accordée aux transformations logiques. Les transformations sont instrumentées pour produire des certificats puis ceux-ci sont vérifiés par un outil externe: c'est l'approche sceptique. De ce fait, notre méthode est incrémentale et robuste aux modifications apportées au code des transformations. Nous définissons deux formats de certificats; les transformations génèrent des certificats de surface et ces certificats sont traduits en des certificats de noyau qui sont destinés à la vérification finale. L'accent est mis sur la facilité de production des certificats de surface et nous avons fait en sorte qu'ils soient, autant que possible, indépendants des tâches de preuve, facilitant ainsi leur composition et rendant la certification plus modulaire. Les certificats de noyau, au contraire, incluent de nombreux détails tout en restant élémentaires, de sorte que leur vérification est réalisable par un outil simple, dont la confiance est facile à établir. Nous proposons une procédure de traduction d'un certificat de surface en un certificat de noyau qui n'a pas besoin d'être certifiée. Les transformations logiques sont considérées dans une logique d'ordre supérieur avec polymorphisme de type, ce formalisme pouvant être étendu avec des théories interprétées telles que l'égalité ou l'arithmétique entière. Nous appliquons notre méthode à Why3, et notamment à des transformations complexes qui pré-existent à notre travail. Nous implémentons également deux vérificateurs de certificats, le premier reposant sur une approche calculatoire efficace et l'autre s'appuyant sur un encodage superficiel des tâches de preuve dans le framework logique Lambdapi, donnant ainsi de fortes garanties de sa correction.
Résumé fourni dans les métadonnées — anglais
Auteurs indexés : Quentin Garchery. Source : tel-03560564, version 1.
In various provers and deductive verification tools, logical transformations are used extensively in order to reduce a proof task into a number of simpler tasks. Logical transformations are often part of the trusted base of such tools. In this thesis, we develop a framework to improve confidence in their results. We follow a skeptical} approach: transformations are instrumented to produce certificates that are checked by a third-party tool. Thus, we benefit from a modular approach that is also robust to changes in the source code of the transformations. We design two kinds of certificates. Transformations produce surface certificates} that are then translated to kernel certificates} which are destined for final verification. We made sure that surface certificates are easy to produce. Moreover, surface certificates are as independent of the transformation application as possible and this makes for a modular certification. On the contrary, kernel certificates include numerous details about the transformation application and are kept elementary. This helps to define simpler checkers and establish their correctness. We propose a translation procedure from surface certificates to kernel certificates which does not need to be trusted. Logical transformations are considered in a higher-order logic, with type polymorphism and built-in theories such as equality and integer arithmetic. We apply our framework to Why3 and use it to instrument pre-existing and complex transformations. Additionally, we implement two certificate checkers. The first one follows an efficient computational approach while the second is based on a shallow embedding of proof tasks inside the logical framework Lambdapi, thus exhibiting formal guaranties of its correctness.
Les résumés restituent les métadonnées du dépôt. Pour apprécier les résultats, la méthode et les limites du travail, consultez le document et son contexte. Métadonnées HAL sous CC0.