Hosei University · Tokyo, Japan
AIRI Lab is the research group behind AIPL and AICE. We design programming languages for concurrent systems that call AI models as an ordinary part of computation — and we check them twice: with machine-verified proof, and with measurement on real model traffic.
Yasushi Kodama
Professor; Director, Data Science Center
Hosei University, Tokyo, Japan
Principal investigator. Language design, the Rocq (Coq) development, the measurement harnesses.
Affiliation, on the public record: the Data Science Center of Hosei University lists Yasushi Kodama as its Director — www.dsc.hosei.ac.jp (appointment notice, 1 April 2024). He is a Professor in the Faculty of Business Administration; his research is in programming languages and formal verification.
The group is the principal investigator together with students in his laboratory at Hosei University. Faculty collaborators at other universities are joining as named co-investigators.
Hosei University is an accredited private university in Tokyo. This is academic, non-commercial research; the code and the proofs are released publicly.
AIPL is an actor language whose type system tracks side effects as
capabilities — !{ai, net, io, mut, time, mem, fs, log}.
Effects propagate through now and await, so a method
that does not declare ai cannot reach a model call even
indirectly.
Type soundness, type safety and deadlock freedom are proved in Rocq (Coq) across three fragments. The boundary of the guarantee is formal too: for the largest fragment we proved that deadlock is admitted, rather than quietly leaving it out.
When does a graph of small, individually verified LLM nodes beat one large prompt? We derived the break-even conditions and measured them — including the case where a per-node verifier detects a defect but cannot repair it.
AIPL runs on bare metal: Embedded Xinu on Raspberry Pi 3/4/5, with a small language model resident in the kernel, and a real multi-hop wireless MANET used for disaster-evacuation research.
k·p^(k-1) < 1 under per-call pricing, and whenever
k ≥ 2 and p < 1 under token pricing — with the
caveat we state ourselves: the formula assumes failures are independent, and says
nothing about a defect that recurs at the same node every time.
ai_call returns in about 0.4 s with no network at all.
coq/ on the make-src-base branch.
The group has written about 84 technical reports (roughly 990 pages), most of them in Japanese. A selection:
The full report archive is access-controlled. PDFs are available on request.
Yasushi Kodama, Data Science Center, Hosei University, Tokyo, Japan — yass@hosei.ac.jp. You can also register on this site to reach the members area.