Foundations and Applications of Modal Type Theories
Notice bibliographique
Résumé
Over the past few decades, type theories as mathematical foundations have been extensively studied and are well understood.Many proof assistants implement type theories and have found important applications to provide critical security guarantees.In these applications, users often write meta-programs, programs that generate other programs, to implement proof search heuristics and improve their work efficiency.However, as opposed to the deep understanding of type theories, it remains unclear what foundation is suitable to support meta-programming in proof assistants.In this thesis, I investigate modal type theories, a specific approach to this problem.In modal type theories, modalities are a way to shallowly embed syntax into the systems, so users can write meta-programs that manipulate syntax through these modalities.I explore two different styles of modal systems.In the first part, I investigate the Kripke-style systems, which faithfully model the familiar quasi-quoting style of metaprogramming.I develop an explicit substitution calculus and scale it to dependent types, introducing Mint.I prove strong normalization of Mint, which implies its logical consistency, using an untyped domain model.Nevertheless, the Kripke-style systems only support composition and execution of code, and they cannot easily support a general recursion principle on the structure of code.To support such a general recursion principle, I develop the layered style, where a system is divided into nested layers of sub-languages.The layered style scales quite naturally to dependent types, introducing DeLaM.DeLaM allows users to compose, execute and recurse on dependently typed code.I prove that DeLaM is weakly normalizing and its convertibility problem between types and terms is decidable.Hence, DeLaM provides a type-theoretic foundation to support type-safe meta-programming in proof assistants.i Abrégé Au cours des dernières décennies, les théories des types comme fondements mathématiques ont été étudiées en détails et sont maintenant bien compises.Plusieurs assistants de preuve implémentent les théories des types et ont établi des applications pour fournir d'importantes garanties de sécurité.Dans ces applications, les utilisateur écrivent des méta-programmes, c'est-à-dire des programmes générant d'autres programmes, dans le but d'implémenter des heuristiques de recherche de preuve et ainsi d'améliorer l'efficacité de leur travail.Néanmoins, malgré la grande compréhension des théories des types, les fondements adéquats pour la méta-programmation dans les assistants de preuves demeurent incertains.Dans cette thèse, j'investigue les théories des types modaux, une approche spécifique tentant de résoudre ce problème.Dans les théories des types modaux, les modalités fournissent une encapsulation superficielle de la syntax dans le système, permettant aux utilisateurs d'écrire des méta-programmes qui manipulent la syntaxe à travers ces modalités.J'explore deux styles distincts de systèmes modaux.D'abord, j'explore les systèmes de style Kripke, qui modélisent fidèlement l'approche familière de méta-programmation appelée quasi-citation (traduit de l'anglais quasi-quotation).Je définis un calcul de substitution explicite, puis l'étends aux types dépendents, menant à l'introduction de Mint.Je prouve la normalization forte de Mint, qui implique sa consistence logique, en utilisant un modèle de domaine non-typé.Cependant, les systèmes de styles Kripke supportent seulement la composition et l'éxécution de code, et permettent difficilement le support d'un principe général de récursion sur la structure du code.Afin de supporter un principe général de récursion, je développe le style stratifié, dans lequel un système est séparé en strates imbriqués de sous-langages.Le style stratifié s'étend de façon naturelle aux types dépendents, menant Publications•
Récupéré en direct depuis OpenAlex et désinversé. Les résumés ne sont pas conservés dans cette base de données : les index inversés représentent 8,6 Go des 9,3 Go de texte de la base, et le serveur dispose de 13 Go libres.
Comment cette classification a été obtenuedéplier
Prédiction machine sur la base complète
Imitation des enseignantsNi prévalence calibrée, ni vérité terrain. Validation humaine à venir. Le volet Gemma est une étiquette directe du modèle pour chaque travail de la base, lue sur la notice réduite au titre. Le volet Codex est un classifieur appris des 10 348 étiquettes directes de Codex et calibré sur les taux pondérés de l'échantillon; les champs sans appui suffisant ne portent aucun appel Codex. Le mode candidate est l'union des deux volets; le consensus est leur intersection. Ces sorties portent le statut machine_predicted_unvalidated et ne sont pas des étiquettes humaines.
Scores du classifieur distillé par catégorie (deux têtes)
| Catégorie | Codex | Gemma |
|---|---|---|
| Métarecherche | 0,003 | 0,009 |
| Méta-épidémiologie (sens strict) | 0,001 | 0,001 |
| Méta-épidémiologie (sens large) | 0,001 | 0,002 |
| Bibliométrie | 0,003 | 0,004 |
| Études des sciences et des technologies | 0,003 | 0,008 |
| Communication savante | 0,007 | 0,015 |
| Science ouverte | 0,001 | 0,004 |
| Intégrité de la recherche | 0,001 | 0,006 |
| Charge utile insuffisante (le modèle a refusé de juger) | 0,013 | 0,002 |
Scores machine (provisoires)
Les deux têtes enseignantes du modèle étudiant, lues sur ce travail. Un score ordonne la base pour la relecture; il n'affirme jamais une catégorie, et le statut de validation accompagne chaque rangée tel quel.
Scores de référence d'un modèle non mature (critères de maturité non atteints, 7 itérations). Un score ordonne; il n'affirme jamais une catégorie.
score_only:v0-immature-baseline · tel quel depuis la passe de notation : score_only signifie que le nombre peut ordonner les travaux, et qu'aucune étiquette de catégorie n'en découleClassification
machine, non validéePrédiction automatique; un appel candidat d’une seule source (Gemma direct ou Codex distillé), pas un consensus.
Le détail, modèle par modèle et score par score, se trouve en fin de page sous « Comment cette classification a été obtenue ».