Kodama Studio / Research
型付き Actor に基づく知的計算環境 AICE と、その記述言語 AIPL（ABCLc+） に関するレポートを、 作成日付の新しい順に並べています。
AICE は、AI エージェント・モデル呼び出し・記憶・ツール・UI・Web エンドポイント・OS サービスを すべて actor として統一的に扱う知的計算環境の構想です。AIPL はその記述言語で、 ABCL/1 の系譜にある actor-first 言語 ABCLc+ の実装を基礎としています。
収録しているのは、言語仕様と型システムの設計、型健全性の Coq による機械検証、 OS 記述・群ロボット・多エージェント進化計算といった応用構想の各レポートです。 すべて PDF で、このサイト上から直接読めます。
進行定理が二択になる ---- 効果と期限つきの定式化
第1版が「仮想の部分言語」について証明したのに対し、本稿の AIPL−2 は現行実装の部分集合です。実装から証明可能な範囲を切り出し、効果注釈と期限つきで定式化しました。主結果は進行定理が二択になること ---- 期限のない待ちを構文から外すと、待ちが簡約として進むため「未解決 future の await でブロック」の枝が消え、系としてデッドロック自由が言えます。ただしこれはデッドロックが有限時間の失敗に変換されるということで、失敗が消えるのではありません。効果を future の型に載せると「実時間側はエージェント側を待てない」が定理として出ます。この定式化により、実装が now を future+await に分けると効果検査を逃れる穴を持つことも判明しました（再現を確認済み）。
可能性、メリット、デメリット
小林直樹の三十余年の研究（線形型、デッドロック自由な型システム、汎用型システム、資源使用解析、高階モデル検査と交差型の等価性、述語抽象と CEGAR、HFL、CHC への還元、サイズ型）を、先の「言語仕様の検討」が未解決として残した穴に突き合わせます。結論は「全て取り入れることは可能でも望ましくもない」。ただし返信先の一級化は線形型で、where の検証は述語抽象と CEGAR で、応答時間の上界はサイズ型で閉じます。最大の代償は説明可能性 ── 還元して解くと反例が AIPL の言葉で出なくなることです。
線形論理による並行オブジェクト指向言語から、時相論理の高階モデル検査まで
DBLP の記録（全229件）に基づき、1992年から現在までを五期に分けて辿ります。初期の並行オブジェクト指向言語の基礎づけは線形論理（ACL, OOPSLA 1994）であり、時相論理はむしろ後期に検証の対象として現れます。初期は書くための論理、後期は検証するための論理という転回を軸に読み、本プロジェクトの AIPL との接点も三点挙げています。
ABCL/1 の機構の再導入と、分散 AI エージェント／実時間 OS という目的から
ABCL/1 が持っていた express mode（割り込み）と where（状態依存の受理条件）を AIPL に戻すと何が起きるかを、構文・実装・型システム・形式的保証の四層で検討します。さらに分散 AI エージェント言語と実時間 OS 記述言語では要求が正反対であるため「一つの中核と二つのプロファイル」に分けるべきだと論じ、理想仕様案として完全な文法・型付け規則・効果の格子・プロファイル制約を明文化しています。
機能とモデルの観点からの比較
源流である ABCL/1（Yonezawa, Briot, Shibayama, OOPSLA 1986）と現在の AIPL を比較します。AIPL は三種のメッセージ送信（past / now / future）をほぼそのまま継承した一方、express mode・返信先の一級性・where つきパターン受信の三つを失っていることを整理し、両者の差が「並行性の表現力を削って静的な保証を得た交換」であると結論づけます。
現状の文法・使い方・サンプル 8 本
AIPL を実際に書く人のためのガイドです。5 分で動かす手順から、字句・型・式・優先順位・文、アクターと通信（send / now / future / reply / select）、期限付きの待ち、効果注釈、外部公開、組込み関数とその効果までを収録しています。動かして確認したサンプル 8 本をソース全文と実行結果つきで解説し、処理系の環境変数（AIOS_STRICT_DEADLINE で型健全性の定理が成立する範囲に留まる、など）と優先順位表、よくある落とし穴を付録にまとめました。
reply の引数から型は決まるか
「メソッドの戻り値型は reply の引数から推論できないか」という問いに答えます。推論は可能だが決まらない場面が6つあることを示し、推論と省略可能な戻り値型注釈の両方を実装しました。その過程で、整数演算が実行時に float を返していた preservation の破れを、型検査結果と実行値を突き合わせる差分テストによって発見・修正した記録も含みます。
証明が成立する範囲 AIPL− の定式化と機械検証
AIPL から部分言語 AIPL− を切り出し、その型健全性（保存・進行）と型安全性を Coq で機械検証した記録です。アクターの状態ストア、メールボックス、future 表、動的生成をすべて含みます。進行定理を「値・簡約・await 待ち」の三択として述べてデッドロックが型だけでは排除できない境界を明示し、そのうえで哲学者の食事問題について個別にデッドロック自由を証明しています。
Coq による形式化と機械検証
AIPL の型推論の土台にある Hindley–Milner 型システムについて、推論の健全性と、多相・再帰を含むコアの保存・進行を Coq で検証しました。一般化に Damas–Milner の側条件を課すことで算術的体系と宣言的体系が実際に異なり、定理が discharge すべき義務を持つようにしています。occurs check の正当性も証明しています。
上記レポートの英語版（証明のスケッチは簡潔）
日本語版と同じ二つの Coq 開発（推論の健全性、多相コアの保存・進行）を英語で簡潔にまとめたものです。文法・型定義・推論規則を通常の記法で併記しています。末尾の節で、二つの定理が何を保証し何を保証しないかを明示しています。
高階モデル検査における両者の等価性をめぐるサーベイ
「モデル検査を使った型推論の論文はあるか」という問いに答えるサーベイです。答えはあるが予想される形とは違い、モデル検査を型推論の道具として使うのではなく、高階再帰スキームのモデル検査と交差型の型検査が同じ問題であることが示されています（Kobayashi–Ong, LICS 2009）。掲載書誌はすべて DBLP で実在を確認しています。
Capability 推論による役割分担・冗長化・アクター移動
6 軸アーム DOFBOT を 1 軸 1 台の Xinu で制御する設計です。中心となる主張は一つ ── アクターの効果集合から、配置・複製可否・フェイルオーバの手順が機械的に決まる。純粋なアクターは自由に複製でき、外部作用を持つアクターは同時に一つしか存在してはならない、つまりフェイルオーバとは Capability の移譲そのものである、と論じます。
現状評価、効果の見積もり、実機構成の提案
アーム型ロボットを Raspberry Pi 経由で制御する構成で、Xinu ベースの 12 台メッシュが効果を発揮するかを検討します。結論は関節サーボループには効果がなく むしろ有害、一方で動作計画・学習・分散知覚・冗長性には効くが台数に比例しない（12 ノードで 4〜6 倍程度）。現状の Xinu が I2C・PWM・GPIO ドライバを持たない点も含め、根拠を示して実機構成を提案します。
Raspberry Pi 4 / Cortex-A72 向け Embedded Xinu
Embedded Xinu を Raspberry Pi 4（BCM2711 / Cortex-A72, AArch64）へ移植した実装について、OS として何が足りないかを網羅的に洗い出したアセスメントです。同日付の短縮版（5ページ）とは別文書で、こちらが詳細版にあたります。
rpi3(A53) / rpi4(A72) / rpi5(A76) 実カーネルの精査
AIPL で記述してアーム型ロボットを 12 台の Xinu ノードで制御するフィジカル AI 向け RTOS 構想の前段として、現行 Xinu 3 ポートの実カーネルをファイル・行レベルで精査しました。結論は3 ポートは別物のカーネルであること ── rpi3 はクラシックなプリエンプティブ優先度スケジューラを持つ一方、他は構成が異なることを具体的に洗い出しています。
フィジカル AI（アーム型ロボット）向け分散 RTOS への道筋
ベアメタル Embedded Xinu を、AIPL で記述するフィジカル AI 向けリアルタイム OS へ発展させ、最終的にアーム型ロボットを 12 台の Xinu ノードで制御する構想の道筋を述べます。3 世代 Raspberry Pi クラスタの実測を踏まえ、RTOS 化に必要な改良項目を整理しています。
3 世代 Raspberry Pi クラスタでの負荷分散設計探索と sim-to-real gap
ソフトウェアの設計を進化計算で探索し、各候補を実機の Xinu メッシュで実際に走らせて適応度を測る枠組みを構築しました。対象は N-Queens(N=14) を A53/A72/A76 の異種 3 ボード（計 12 コア）へどう配分すれば makespan が最小になるかという実行設計問題です。実機の実測から作ったコストモデルと、シミュレーションと実機の乖離を論じます。
案 B: セル密度に対する情報拡散の遅延と到達率／多賀 2021 第 4 章の 4 エージェントを実 Embedded Xinu・実 IBSS 無線へ
多賀祥平 博士論文（2021）の避難支援 MANET を、実 Embedded Xinu 機（Raspberry Pi）と実 ad-hoc 無線の上で評価する実験系を設計・実装した報告です。出発点は否定的な発見でした ── 既存の AIPL 実装は「そのまま実機へ載る」と自称していたが載らない。AIPL→C コンパイラがリモート送信を無言で誤訳する、Xinu に TCP クライアントが無い、アクタランタイムが同期リモート呼び出しを再入できない、という 3 点が独立に致命的でした。
東京都荒川区 実地図・大規模火災シナリオ（多賀 2021 第 6 章）を「1 避難者 = 1 台の soft-Xinu / AIPL ノード」として実装
多賀 2021 第 6 章「大規模火災シナリオ」を、東京都荒川区の実道路網（OpenStreetMap 由来、266 頂点・4 避難所）上で再現した実験レポートです。各避難者を 1 台の soft-Xinu / AIPL ノードとみなし、第 4 章の 4 エージェント（情報 / ノード管理 / 情報拡散 push, hop 1 / 情報収集 pull）を各端末に定義して、MANET 情報共有の意味論を忠実に実装しました。
phone_node_fire.abcl — 上記再現実験の付録
上の再現実験で各避難者端末に載せた 4 エージェントの AIPL ソースコード全文です。InfoAgent / NodeManager / DiffusionAgent（push, hop 1）/ CollectingAgent（pull）の4 アクターがどう書かれているかを、実際のコードで示しています。
東京都荒川区 266 頂点/4 避難所・論文 図 6.2 / 6.3.2 との比較
同じ第 6 章を、ブラウザ実装として実地図上に再現しました。避難者は最寄り避難所へ最短経路で避難し、通行不能点（火災）に接触すると引き返して経路を再構成します。避難支援システムの利用／不使用を接触回数で比較し、N = 50〜200 人・各 50 回平均ですべての条件でシステム利用により接触回数が約半減し、論文値と同水準を得ました。
ドローンを用いない、携帯端末メッシュ上の情報拡散シミュレーション
災害時に基地局が失われた状況では、避難者が携帯する端末そのものを無線ノードとする MANET と、その上を渡り歩く移動エージェントによる情報拡散が有効です（多賀 2021 第 4 章）。本稿はこの移動エージェント方式を AIPL のアクターと soft-Xinu で実装し、評価したものです。
多群 PSO による安全性検査カバレッジ向上の追試
「Enhancing Safety Checking Coverage with Multi-swarm Particle Swarm Optimization」を追試し、報告された効果がどこまで再現するかを評価したレポートです。以下の拡張研究5本の出発点にあたります。
反例局所のペナルティがなぜ効かないか、どう直すか
追試から出た拡張研究その1。反例の近傍だけにペナルティを与える素朴な方式がなぜ探索を改善しないかを示し、カバレッジで誘導する更新則を提案しています。
多群探索に大域的な新規性報酬を与える
拡張その2。局所的な新規性ではなく大域的な新規性に報酬を与えることで、群が同じ領域を重複して探索する問題に対処します。
フロンティアを保持したまま再開する
拡張その3。再スタートのたびに探索フロンティアを捨てるのではなく保持することで、逐次的なモデル検査の効率を上げます。
計算予算とカバレッジのスケーリング則
拡張その4。投入した計算予算に対してカバレッジがどう伸びるかを測り、スケーリングの形を明らかにしたコスト・カバレッジ研究です。
カバレッジを平均でなく分布で測る
拡張その5。モデル検査のカバレッジを平均値で語ることの問題を指摘し、分布そのものを見る強度指標を提案しています。
ドローンを中継ノードとして使うとき、どこをどう飛ばせば情報拡散が最も改善するかを扱います。固定巡回・需要追従などの軌道方針を比較し、避難者の分布に応じた配置の効果を定量化しました。
実機無線 (ns-3) 下での「接触回数・死亡者数」の再評価
通信層（ns-3 の実無線モデル）と避難行動シミュレーションを統合し、理想通信を仮定した場合と比べて接触回数・死亡者数がどう変わるかを再評価しました。通信の劣化が避難結果にどこまで波及するかを示します。
臨界普及率・フリーライド・私的便益の ns-3 検証
避難支援システムを何割の人が使えば効果が出るのか（臨界普及率）を ns-3 で検証しました。使わない人も恩恵を受けるフリーライドの構造と、使う人自身の私的便益を分けて評価しています。
延焼するフロントを先読みする避難経路の ns-3 検証
火災front が時間とともに広がる状況で、現在の通行不能点だけを見て回避するのではなく延焼の先を読んで経路を選ぶ方式を検証しました。先読みの有無で避難成功率がどう変わるかを ns-3 上で比較しています。
多賀 (2021) 7.2.1 節「Small MANET の問題」の定量評価
多賀博士論文が将来課題として挙げた「疎な MANET ではドローンを中継ノードとして補強する」という仮説を、ns-3 で定量的に検証しました。避難者端末を Wi-Fi アドホックノード（通信半径 50 m、移動速度 1 m/s）としてモデル化し、Information Diffusion Agent を store-carry-forward 型で実装。避難者 50〜200 人 × ドローン 0/3/5 台の計 120 試行で効果を測りました。
Mac + Embedded Xinu / Pi 5
管理ノード（Mac）とワーカーノード（Embedded Xinu を載せた Raspberry Pi 5）から成る AICE システム上で、型推論クリーンな AIPL で書いた二つの古典問題を分散実行してベンチマークを取りました。N-Queens は第 1 行の列で探索空間を分割して振り分け、哲学者は 5 人 × 50 食の所要時間を測定。いずれもガベージコレクションなしで動きます。
ベアメタルの Embedded Xinu を載せた Raspberry Pi を WiFi MANET で結び、その上で N-Queens を実際に分散実行した報告です。OS もネットワークも自前という条件下で、AIPL で書いた探索がどう動くかを実測しています。
上記の英語版
The English version of the report above: N-Queens distributed over a real WiFi MANET of bare-metal Embedded Xinu nodes, with the search written in AIPL.
型推論を通した AIPL で書いた食事する哲学者を、ベアメタル Xinu 上で実行した報告です。並行性の古典問題が、自作言語・自作 OS の組み合わせで実際に動くことを示しています。
哲学者 5 名を Pi4（AIPL JIT）と Pi3（Chandy–Misra）に分けて実行
哲学者を 2 台の実機に分散させ、一方は AIPL の JIT、他方は Chandy–Misra アルゴリズムで動かした報告です。実機間の無線を挟んだ分散環境で、フォークの排他がどう保たれるかを見ています。
BCM43455 ---- スキャンから WPA2 接続・DHCP・ping 疎通まで
Embedded Xinu 上で BCM43455 の WiFi ドライバをゼロから書き起こした実機検証レポートです。ファームウェア投入、スキャン、WPA2 での接続、DHCP によるアドレス取得、ping 疎通までを実機（arm-rpi3 platform）で確認した記録を、詰まった箇所とその原因とともに残しています。
Embedded Xinu (Raspberry Pi 3) 上での計測
ガベージコレクションと連動させた分散 N-Queens の実機ベンチマークです。GC の起動タイミングが分散探索のスループットにどう効くかを計測しました。
Raspberry Pi 3 B+ 実機で 50 食 x 5 人を計測
デッドロック回避の二方式を実機で比較しました。素朴な資源階層法と Chandy-Misra 法をAIPL アクターで実装し、Raspberry Pi 3 B+ 上の Embedded Xinu で 50 食 x 5 人を走らせて計測しています。平均値ではなく分布で見ることで、両者の差がどこに出るかを示しました。
Mac + Raspberry Pi 3 の混成構成、AIPL アクター負荷分散器
Mac と Raspberry Pi 3（Embedded Xinu）を混ぜた構成で N-Queens を分散実行し、AIPL アクターで書いた負荷分散器の効きを計測したレポートです。同時期の WiFi MANET 版とは構成が異なり、こちらは有線・混成環境での評価にあたります。
Raspberry Pi Zero 2 W / Raspberry Pi Pico (RP2040)
Xinu-rpi プロジェクトの移植計画書です。Raspberry Pi Zero 2 W と Pico (RP2040) を対象に、何を移植し何が障害になるかを事前に洗い出しています。
ランク階層フラグメントの Coq 機械検証
注意 ---- ここでの AIPL は Array-Inspired Pipeline Language であり、本一覧の他の項目にある アクター言語 AIPL（ABCLc+）とは別の言語です。配列指向パイプライン言語に対し、型（＝ランク）システムを与え、ランクで層別された入れ子配列と整数ランク演算子からなる中核フラグメントについて進行・保存・型安全性・決定性を証明しました。全定理は The Rocq Prover (Coq) 9.1.0 で機械検証済みです。
論文草稿
複数の大規模言語モデルをエージェントとして協調させ、進化計算ループで問題解決を行うAIPL（AI Programming Loop）システムを提案します。題材はブラウザ向け単一 HTML アプリの段階的構築で、自動テスト合格率とコード簡潔さを fitness としました。パイロット実験で「多エージェントは単一より速い」「再現性が高い」「過去の成功例の注入が収束を早める」の 3 仮説を統計的に検証しています。
実験題材・ログ形式・解析パイプラインの設計と実装
上記の仮説を学術的に評価するための実験基盤を、設計から実装まで一通り整備した報告です。進化速度・再現性・履歴からの学習という 3 つの仮説を測るための実験題材、ログ形式、解析パイプラインを定めています。上の論文草稿の土台にあたります。
Actor-first 言語による教育用・研究用 OS カーネルの設計
教育用 OS である Xinu の構成要素を AIPL の actor に対応づけ、プロセス管理・mailbox・スケジューリング・デバイスドライバ・システムコール・メモリ管理・割り込み処理をどう記述するかを検討します。システムコール引数、デバイス capability、プロセス間メッセージ、カーネルサービスのインタフェースを型で検査する設計を提案しています。
Actor 型、Protocol、Tool、Memory を統合する自己記述的 AIOS
AICE を単なる AI 実行基盤ではなく、自己の構成要素を観測・記述・検査・再構成できるメタ環境として捉える研究構想です。構成・型・capability・protocol・実行 trace・性能・失敗・変更履歴を第一級データとして扱い、reflection / introspection / orchestration / verification / evolution の五層として設計します。
型付き Actor と局所通信による群ロボット制御の設計
多数の単純なロボットが局所通信と局所観測で協調する群ロボットシステムを、AIPL で記述・実装する構想です。各ロボット・基地局・環境センサ・タスク管理器を actor として表現し、位置・速度・電池・センサ値・近傍情報・タスク割当を型で区別することで、誤った制御メッセージや capability 違反を防ぐ設計を提案しています。
Actor、Protocol、Memory、Review による安全な AI Orchestration
planner・solver・reviewer・memory・tool・model router といった役割の協調として AI システムを設計するとき、単純な prompt chaining では信頼性を確保しにくい理由を論じます。問題解決を「型付きメッセージを交換する actor 群による protocol-guided search」として捉え、AI の非決定性そのものを消すのではなく、非決定性の周囲に検査可能な構造を与える立場を採ります。
AIPL 記述言語、型の必要性、AIOS 実行基盤の考察
AICE の基本構想を、記述言語 AIPL との関係から整理した中心的なレポートです。AI アプリケーションを単一の巨大な関数や逐次スクリプトではなく、型付きメッセージを交換する多数の actor の協調として捉えます。外部 API・非決定的なモデル出力・並行実行・remote actor・長時間処理を含むため、動的 dispatch だけでは安全性と保守性を確保できないことを論じます。
実装に基づくレポートと Coq 形式化
実装に基づいて ABCLc+ の型システムを整理し、Coq で検証可能なコア体系として示したレポートです。Hindley–Milner 風の型変数・型スキーム・単一化・primitive overload・actor メソッド表・now・future/await・実行時セッションプロトコル検査を備える一方、any・remote actor・sender・戻り値型に未完成の動的境界が残ることを明示しています。
Yasushi Kodama, Faculty of Business Administration, Hosei University
AICE を英語で提示した最初の論文です。値の型・actor の型・通信の型からなる三層の型システムを導入し、型安全性だけでは非同期通信の正しさを保証できないことを示します。選択受信の操作的意味論を形式化し、プロトコル水準の保証のためにセッション型を任意で統合する案を提案しています。この一覧の中で最も早い日付のレポートです。