27 papers
Dit artikel bewijst dat het geven van een rechter-actegorie met hom-objecten equivalent is aan het geven van een rechter-verrijkte categorie met copowers, een generalisatie die essentieel is voor de semantiek van hogere-orde procesdoorgeven in de concurrente taal CaMPL.
Deze paper presenteert de eerste grootschalige empirische studie naar het gebruik van drijvende-kommaberekeningen in statisch getypeerde GitHub-repositories, waarbij een dataset van 10 miljoen functies wordt vrijgegeven om de representativiteit van bestaande benchmarks te evalueren en toekomstige analyse-technieken te verbeteren.
Dit paper introduceert Turn, een gecompileerde, actor-gebaseerde programmeertaal die LLM-inferentie als een getypeerde primitief behandelt en via taalgebouwde constructies zoals cognitieve typeveiligheid en een capability-gebaseerd identiteitssysteem, kritieke invariants voor autonome agenten garandeert in plaats van ze als applicatieniveau-conventies te laten bestaan.
Dit paper introduceert Arbiter, een framework dat formele regels en multi-model LLM-scouring combineert om interferentiepatronen in systeemprompts van coderingsagenten te detecteren, waarbij het verschillende kwetsbaarheden blootlegt die vaak worden gemist door traditionele methoden.
Dit artikel formaliseert het concept van idempotente terugwaartse slices en presenteert een correct en efficiënt algoritme voor het extraheren ervan uit GSA-gecodeerde programma's, wat leidt tot een nieuwe, spaarzame optimalisatie voor het verkleinen van de codegrootte door niet-aaneengesloten instructies te samenvoegen.
Dit paper introduceert vLLM Hook, een open-source plug-in die programmabele toegang biedt tot de interne staten van vLLM-modellen, waardoor zowel passieve analyse als actieve interventie mogelijk wordt voor toepassingen zoals het detecteren van prompt-injecties en het verbeteren van RAG-systemen.
Dit artikel introduceert een methode die Syntax Guided Synthesis en Temporal Stream Logic combineert om databewuste tijdspecificaties en transformaties te leren uit uitvoeringstraces, wat leidt tot een robuustere en veel efficiëntere synthese van reactieve programma's dan bestaande passieve leerbasislijnen.
Dit paper introduceert PolyBlocks, een modulaire MLIR-gebaseerde compilerinfrastructuur voor AI-chips en -frameworks die via geautomatiseerde optimalisaties en analytische kostenmodellen prestaties levert die concurreren met of zelfs de beste vendor-bibliotheken en bestaande compilatoren zoals Torch Inductor en XLA overtreffen.
Dit paper introduceert drie complementaire benaderingen om creatieve activiteiten in verschillende domeinen beter te documenteren en te interpreteren door de intentie en relaties achter staatveranderingen vast te leggen, in plaats van alleen de ruwe wijzigingen te registreren.
Dit paper introduceert EAGLE-Pangu, een reproduceerbaar systeem dat boomgestructureerde speculatieve decoding op Ascend NPUs veilig implementeert voor Pangu-modellen, waardoor de doorvoersnelheid aanzienlijk wordt verbeterd ten opzichte van traditionele methoden.
Deze paper ontwikkelt een theorie van abstracte GSOS-specificaties voor hogere-orde talen die compositionaliteitsbewijzen mogelijk maakt door het Turi-Plotkin-raamwerk uit te breiden naar een hogere-orde setting, waarbij de operationele semantiek wordt weergegeven als gepunte hogere-orde GSOS-wetten.
Dit paper introduceert VyZX, een geverifieerde bibliotheek die inductieve grafieken en bewijshulpmiddelen combineert om de correctheid van de ZX-calculus voor kwantumcomputatie formeel te verifiëren en een visuele IDE-integratie biedt voor het redeneren over diagrammen.
Dit artikel introduceert RightTyper, een hybride aanpak die statische analyse combineert met adaptief gesampleerde dynamische uitvoering om nauwkeurige Python-typeannotaties te genereren met slechts ongeveer 27% runtime-overhead, waarmee de beperkingen van eerdere statische, dynamische en AI-gebaseerde methoden worden overwonnen.
Dit artikel introduceert een volledig symbolische theorie voor lokaalheidsanalyse die cache-prestaties als polynomen afleidt en binnen een milliseconde een voorspelling van cache-misses levert met 99,6% nauwkeurigheid voor diverse wetenschappelijke kernels.
Deze lezingen notities bieden een beknopte inleiding in elementen van de categorietheorie, specifiek gericht op toepassingen in functioneel programmeren zoals initiele algebra's voor datatypes en monaden voor effecten, en bevatten talrijke opgaven met oplossingen.
Deze paper introduceert Linear Layouts, een nieuwe aanpak die tensorindelingen modelleert met lineaire algebra over om flexibele en efficiënte generatie van tensorberekeningen mogelijk te maken, de complexiteit van conversies te reduceren en de foutgevoeligheid in bestaande compilersystemen zoals Triton te verminderen.
Dit paper introduceert ZipLex, een formeel geverifieerd framework voor lineaire, omkeerbare lexing dat gegarandeerde wederzijdse inversie tussen lexing en printen biedt, lineaire tijdscomplexiteit garandeert via geverifieerde memoïzatie, en aanzienlijk sneller is dan bestaande geverifieerde lexers zoals Verbatim++ en Coqlex.
Dit paper introduceert hybride gestructureerde bewerking, een aanpak die toolbouwers structurele garanties biedt voor betrouwbare hulpmiddelen, terwijl gebruikers toch werken met een vertrouwde tekstuele interface.
Dit artikel analyseert de valkuilen bij het porten van virtuele machines zoals CRuby naar CHERI, waarbij het specifiek ingaat op de conflicten tussen C-idioms en het strengere CHERI-beveiligingsmodel, en biedt werkoplossingen om veiligere VM-implementaties te realiseren.
Dit onderzoek evalueert de effectiviteit van negen state-of-the-art Large Language Models in een functionele programmeringcursus met OCaml door middel van drie nieuwe benchmarks (CodeGen, Repair en Explain), en concludeert dat hoewel deze modellen goed presteren bij het corrigeren van fouten en het beantwoorden van conceptuele vragen, ze minder succesvol zijn bij het oplossen van huiswerkproblemen in deze low-resource taal vergeleken met hun prestaties in Python en Java.