27 articles
Cet article établit l'équivalence entre les actéories droites à objets-hom et les catégories enrichies à copuissances dans des bases monoïdales non fermées et non symétriques, une généralisation motivée par la nécessité de soutenir les processus d'ordre supérieur dans la sémantique du langage concurrent CaMPL.
Cette étude empirique à grande échelle analyse l'utilisation de l'arithmétique à virgule flottante dans des millions de dépôts GitHub de langages typés statiquement, révélant que les benchmarks existants ne reflètent que partiellement la réalité du code et publiant un jeu de données de 10 millions de fonctions pour guider les futures recherches.
Ce papier présente Turn, un langage de programmation compilé et basé sur des acteurs conçu pour les logiciels autonomes, qui intègre nativement la sécurité des types pour les inférences LLM, un modèle de processus isolé, un système d'identité basé sur les capacités et l'absorption de schémas à la compilation pour garantir la fiabilité et la sécurité des agents.
Ce papier présente Arbiter, un cadre d'évaluation combinant des règles formelles et un balayage multi-modèles pour détecter des interférences dans les prompts système d'agents de codage LLM, révélant ainsi des vulnérabilités structurelles et des corrélations entre l'architecture des prompts et les types d'échecs.
Cet article formalise la notion de tranches arrière idempotentes et propose un algorithme efficace pour les extraire sous forme GSA, permettant ainsi une réduction significative de la taille du code par fusion d'instructions non contiguës.
Le papier présente vLLM Hook, un plug-in open-source permettant de programmer les états internes des modèles vLLM via des modes passif et actif pour faciliter des applications telles que la détection d'injections de prompts, l'amélioration du RAG et le pilotage d'activations.
Cet article présente une nouvelle méthode qui étend l'extraction de spécifications à partir de traces d'exécution au-delà des abstractions booléennes en combinant la synthèse guidée par la syntaxe et la logique temporelle TSL pour apprendre des transformations de données et des spécifications temporelles, permettant ainsi de générer des programmes réactifs plus robustes et nettement plus efficaces en échantillons que les approches d'apprentissage passif.
Le papier présente PolyBlocks, une infrastructure de compilation modulaire basée sur MLIR pour les frameworks d'IA et les puces spécialisées, qui génère automatiquement du code haute performance grâce à des pipelines de transformations et des modèles de coût analytiques, démontrant des résultats compétitifs avec les solutions existantes comme Torch Inductor et XLA sur les GPU NVIDIA.
Cet article propose trois approches complémentaires pour surmonter la limitation des méthodes actuelles qui enregistrent les changements d'état sans préserver l'intention créative, en introduisant respectivement une interface basée sur des nœuds pour la gestion d'artefacts GenAI, un vocabulaire d'indices visuels pour l'authoring de visualisations et un modèle de programmation intégrant des histoires sémantiques dans l'état d'interaction.
Le papier présente EAGLE-Pangu, un système reproductible qui adapte le décodage spéculatif arborescent de type EAGLE-3 sur les NPU Ascend pour le backend Pangu, en améliorant le débit de décodage grâce à une gestion explicite du cache, une tensorisation sécurisée et un chemin de vérification fusionné.
Cet article développe une théorie des spécifications GSOS abstraites pour les langages d'ordre supérieur, en introduisant des lois GSOS pointées sous forme de transformations dinaturelles qui garantissent la compositionnalité de la sémantique opérationnelle, comme l'illustrent les calculs SKI et .
Ce papier présente VyZX, une bibliothèque vérifiée permettant de raisonner formellement sur les langages graphiques inductifs, en particulier pour prouver la cohérence des règles de réécriture du ZX-calcul utilisé en informatique quantique.
Le papier présente RightTyper, une nouvelle approche hybride pour Python qui génère des annotations de types précises en combinant l'analyse statique avec des observations d'exécution réelles via un échantillonnage adaptatif, offrant ainsi une qualité supérieure aux méthodes existantes avec une surcharge d'exécution limitée à environ 27 %.
Cet article présente une nouvelle théorie de la localité entièrement symbolique, soutenue par un compilateur capable de dériver des polynômes de performance pour des boucles affines, permettant de prédire avec une précision de 99,6 % le nombre de défauts de cache pour n'importe quelle configuration en moins d'une milliseconde.
Ces notes de cours introduisent brièvement des éléments de la théorie des catégories appliqués à la programmation fonctionnelle, en se concentrant sur les algèbres initiales pour les types de données et les monades pour les effets, tout en proposant de nombreux exercices et solutions.
Ce papier présente « Linear Layouts », une approche novatrice modélisant les agencements de tenseurs via l'algèbre linéaire sur pour permettre une définition générique et des conversions efficaces, réduisant ainsi l'effort d'ingénierie et les bogues dans le backend du compilateur Triton.
Ce papier présente ZipLex, un cadre formellement vérifié en Scala pour l'analyse lexicale inversible et linéaire qui garantit que l'analyse et l'impression sont des inverses mutuels tout en surpassant les solutions existantes en termes de performance et de complexité temporelle.
Ce papier propose l'édition structurée hybride, une approche qui permet aux outils de programmation de bénéficier de garanties structurelles pour un suivi fiable du code tout en offrant aux utilisateurs une interface d'édition textuelle familière et cohérente.
Cet article présente les pièges spécifiques à l'implémentation de machines virtuelles sur l'architecture CHERI, identifiés lors du portage de CRuby, qui découlent de comportements non définis en C supposés valides sur les architectures traditionnelles mais incompatibles avec le modèle de sécurité mémoire de CHERI, tout en proposant des solutions de contournement validées.
Cette étude évalue neuf modèles de langage de pointe dans le contexte d'un cours de programmation fonctionnelle en OCaml, une langue à faible ressources, en utilisant trois nouveaux benchmarks (CodeGen, Repair et Explain) pour démontrer que, bien que ces modèles soient efficaces pour corriger les erreurs et répondre à des questions conceptuelles, ils résolvent moins de problèmes de devoirs que dans des langues à haute ressources comme Python ou Java.