Foundations and Applications of Modal Type Theories
Bibliographic record
Abstract
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•
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
How this classification was reachedexpand
Full frame machine prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. The Gemma side is a direct model label for every work in the frame, read from the title-only record. The Codex side is a classifier learned from the 10,348 direct Codex labels and calibrated to design-weighted sample rates; fields without enough sample support carry no Codex call. Candidate is the union of the two sides; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels.
Distilled classifier scores by category (both heads)
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.003 | 0.009 |
| Meta-epidemiology (narrow) | 0.001 | 0.001 |
| Meta-epidemiology (broad) | 0.001 | 0.002 |
| Bibliometrics | 0.003 | 0.004 |
| Science and technology studies | 0.003 | 0.008 |
| Scholarly communication | 0.007 | 0.015 |
| Open science | 0.001 | 0.004 |
| Research integrity | 0.001 | 0.006 |
| Insufficient payload (model declined to judge) | 0.013 | 0.002 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from itClassification
machine, unvalidatedMachine predicted; a candidate call from one source (direct Gemma or distilled Codex), not a consensus.
How this classification was reached, model by model and score by score, is at the end of the page under "How this classification was reached".