Actegories, Copowers, and Higher-Order Message Passing Semantics
本論文は、CaMPL における高次プロセスのセマンティクスを動機として、非閉かつ非対称なモノイダル基盤においても「右作用圏(右 actegory)」と「コパワを持つ右 enriched 圏」が同値であることを証明したものである。
27 件の論文
本論文は、CaMPL における高次プロセスのセマンティクスを動機として、非閉かつ非対称なモノイダル基盤においても「右作用圏(右 actegory)」と「コパワを持つ右 enriched 圏」が同値であることを証明したものである。
この論文は、静的型付け言語を対象とした大規模な実証研究を通じて、GitHub の公開リポジトリにおける浮動小数点演算の使用状況を初めて包括的に分析し、既存のベンチマークと実世界のコードの類似点と相違点を明らかにするとともに、1000 万個の浮動小数点関数からなるデータセットを公開して将来の技術開発を支援することを目的としています。
本論文は、大規模言語モデルによる推論を型安全なプリミティブとして統合し、信頼性、隔離、永続性を言語レベルで保証する、自律的エージェント向けコンパイル型プログラミング言語「Turn」の設計と実装を提案しています。
本論文は、LLM ベースのコーディングエージェントのシステムプロンプトにおける干渉パターンを検出するフレームワーク「Arbiter」を提案し、主要なベンダーのプロンプトに多数の脆弱性を発見し、プロンプト構造と失敗クラスの相関やマルチモデル評価の重要性を実証した。
この論文は、一般的な制御フローグラフに適用可能な健全かつ効率的な「冪等バックスライス」の定式化と抽出アルゴリズムを提案し、これを用いて非連続な命令シーケンスをマージする疎なコードサイズ削減最適化を実現し、LLVM テストスイートにおいて最大 7.24% のコードサイズ削減を達成したことを報告しています。
本論文は、vLLM 内のモデル状態へのアクセスを制限する既存の課題を解決し、受動的な状態監視と能動的な生成介入を可能にするオープンソースのプラグイン「vLLM Hook」を提案し、その有効性を提示するものである。
本論文は、Syntax Guided Synthesis 技術と TSL(Temporal Stream Logic の有限接頭辞解釈)を組み合わせることで、ブール値抽象化の限界を超え、データ変換と時制仕様を同時に学習し、より頑健かつ効率的にリアクティブプログラムを合成する手法を提案しています。
本論文は、MLIR ベースのモジュール型コンパイラ基盤「PolyBlocks」の設計と実装を提案し、その自動コード生成能力が PyTorch や JAX 向けに NVIDIA GPU で Torch Inductor や XLA と同等、あるいはそれ以上の性能を発揮し、個別演算においてもベンダー最適化ライブラリや手書きカーネルと競合する結果を示したものである。
この論文は、GenAI ツール、可視化作成、プログラミング環境といった創造的ドメインにおいて、単なる状態変化の記録を超えて意図や高次な創造的動きを捉えるための、それぞれ異なるアプローチ(ノードベースのインターフェース、視覚的キューの語彙、意味的履歴の埋め込み)を提示するものである。
この論文は、Ascend NPU 上のパングモデル向けに、キャッシュ管理や構造的不変性の保証、融合カーネル対応などによりアクセラレータ環境での安定性を確保した木構造スペキュレイティブデコーディングシステム「EAGLE-Pangu」を提案し、教師モデル単独のデコーディングと比較して最大 2.46 倍の処理スループット向上を実現したことを報告しています。
この論文は、Turi と Plotkin の抽象 GSOS 枠組みを高次言語へ拡張し、高次言語の操作意味論を「指向付き高次 GSOS 法則」として定式化することで、SKI 計算や計算などの高次言語における構成性の保証を可能にする一般理論を構築したものである。
本論文は、図式的な言語の形式検証における課題を解決するため、圏論的な定義から自然に導かれる帰納的グラフ構造を採用し、量子計算の推論に用いられる ZX 計算の健全性を証明するとともに、図形を直接扱える IDE 統合ビジュアライザーを提供する検証済みライブラリ「VyZX」を提案するものである。
本論文は、静的解析と動的実行のハイブリッド手法を採用し、統計的に導かれた適応的サンプリングによってランタイムオーバーヘッドを約 27% に抑えつつ、高精度な Python 型注釈を自動生成する「RightTyper」を提案し、既存の手法を上回る性能を実証したものである。
この論文は、アフィンループネストに対する完全記号的な局所性解析理論とコンパイラ支援手法を提案し、データ移動量の予測精度を 99.6% まで達成しながら、入力サイズやキャッシュ構成に対するキャッシュミス回数をミリ秒未満で推定可能にする技術を示しています。
この講義ノートの論文は、関数型プログラミングへの応用を指針として、データ型と再帰関数の数学的定式化である初期代数と、関数型言語における副作用の枠組みであるモナドについて解説し、多数の演習問題と解答を収録しています。
この論文は、 上の線形代数を用いてテンソルレイアウトをモデル化する「Linear Layouts」という新規アプローチを提案し、Triton への統合を通じて既存手法の課題を解決し、効率的なテンソル計算の実現とコンパイラバックエンドの工数削減を達成したことを示しています。
本論文は、Scala 向けに Stainless 検証器を用いて実装・検証された「ZipLex」を提案し、正規表現と最長一致の性質に加え、トークン列の印刷との相互逆関数性(可逆性)を保証しつつ、従来の検証済み lexer が直面する二次時間計算量の問題を回避して線形時間での処理を実現したことを示しています。
この論文は、ツール開発者に構造的な保証を提供しつつ、ユーザーには慣れ親しんだテキスト編集インターフェースを維持する「ハイブリッド構造化編集」というアプローチを提案し、その実装とケーススタディを通じてプログラミング環境の安全な拡張を可能にすることを示しています。
本論文は、CRuby のポート事例と既存研究の調査に基づき、従来のアーキテクチャにおける C 言語の未定義動作を前提とした VM 実装の慣習が CHERI の厳格なメモリ安全性モデルと衝突して生じる具体的な落とし穴を分類・解説し、その回避策と影響について論じています。
この論文は、OCaml という低リソースな関数型プログラミング言語の教育環境における大規模言語モデル(LLM)の能力を評価し、構文や型エラーの修正、基本的な概念の解説においては効果的であるものの、Python や Java などの高リソース言語に比べて課題解決能力は限定的であることを示すとともに、3 つの新しいベンチマークを提案しています。