Notice bibliographique
Résumé
Recent type systems allow the programmer to use types that describe more precisely the invariants on which the program relies. But in order to satisfy the type system, it often becomes necessary to help the type checker with extra annotations that justify why a piece of code is indeed well-formed. Such annotations take the form of term-level type manipulations, such as type abstractions, type applications, existential package packing and opening, as well as coercions, or casts. While those operations have no direct runtime cost, they tend to introduce extra runtime operations equivalent to n-redexes or even empty loops in order to get to the point where we can apply that supposedly free operation. We show a coercion that is like a pacific Swiss army knife of coercions: it cannot cut but it can instantiate, open, pack, abstract, analyze, or do any combination thereof, reducing the need for extra surrounding runtime operations. And all that, of course, for the price of a single coercion, which still costs absolutely nothing at runtime. This new coercion is derived from Karl Crary's coercion calculus [Crary, 2000], but can also replace Crary and Weirich's vcase [Crary and Weirich, 1999]. It additionally happens to come in handy to work around some limitations of value polymorphism. It is presented in the context of Shao et al.'s Type System for Certified Binaries [Shao et al., 2002]. Other than the coercion itself, another interesting aspect of this work is a slightly unusual proof technique to show soundness of the type erasure using a pure type assignment language, making the no-op nature of our cast more obvious.
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 distillée sur la base complète
Imitation des enseignantsNi prévalence calibrée, ni vérité terrain. Validation humaine à venir. Apprise à partir de 10 348 étiquettes directes de Codex et de 10 348 étiquettes directes de Gemma. Le mode candidate est l'union des têtes enseignantes seuillées; le consensus est leur intersection. Ces sorties portent le statut machine_predicted_unvalidated et ne sont ni des étiquettes humaines ni des étiquettes directes de modèles de pointe.
Scores Codex et Gemma par catégorie
| Catégorie | Codex | Gemma |
|---|---|---|
| Métarecherche | 0,001 | 0,000 |
| Méta-épidémiologie (sens strict) | 0,000 | 0,000 |
| Méta-épidémiologie (sens large) | 0,000 | 0,000 |
| Bibliométrie | 0,000 | 0,000 |
| Études des sciences et des technologies | 0,000 | 0,000 |
| Communication savante | 0,000 | 0,000 |
| Science ouverte | 0,000 | 0,000 |
| Intégrité de la recherche | 0,000 | 0,000 |
| Charge utile insuffisante (le modèle a refusé de juger) | 0,000 | 0,000 |
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 tête enseignante, 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 ».