Web アプリケーションを代表とする多くのシステムは，対話的な操作を行うフロントエンドと共有データを操作するバックエンドを要素に持つものが多い．フロントエンドにはリアクティブプログラミング（RP），バックエンドにはデータベース管理システムが使われ，そこでは複数の一貫性制御を使い分けることが多いものの，これらを組み合わせた場合の研究はこれまで行われてきていない．本研究では，RP言語 SignalJ において一貫性レベルを混在させた分散トランザクションを実現する方法について提案する．分散トランザクションにおいて複数の一貫性レベルを混在させる方法は知られているものの，RP 言語においてはトランザクション内で実行される値更新伝播の範囲が暗黙的になるため，従来の仕組みでは混在一貫性レベルを実現できない．この問題を解決するため，本研究ではアノテーションによりシグナルに付加された一貫性レベルの情報を実行時に用いる新たな混在一貫性レベルの機構を実現した．

Staged computation is a vital means of separating a computation into several stages, such as program generation and execution, enabling high modularity and performance. Programming languages supporting staged computation have been developed to guarantee static type safety for all generated programs. However, the type systems for them quickly become complicated as the computational effects come into these languages, and the resulting type system would be intractable for human programmers.
In this paper, we resolve this tension by presenting an ML-like type inference for a polymorphic type system designed to cover a two-stage programming language with control operators shift0 and reset0. We first extend Oishi and Kameyama’s type monomorphic type system, which is based on Refined Environment Classifiers (classifiers), to safely handle the scopes of generated variables. Our type system has the ML-like let expression, which allows polymorphism in types, classifiers, and effects. We then present a constraint-based type inference algorithm for the extended type system. The constraint-solving problem differs from the standard one in that we need to handle eigen-variable conditions for generated variables, and the constraints over classifiers are inequalities. We show that the satisfiability problem of constraints can be reduced to the problem of detecting strongly connected components for directed graphs induced by the partial order over classifiers. By virtue of our type inference algorithm, a programmer does not have to annotate classifiers in the programs that generate programs using control effects, thus covering many meta-programming idioms.

ビュー更新問題は、データベース研究における古典的かつ未解決の課題であり、ビューに対する更新操作をどのように基底表への適切な更新として変換するかが問われている。本問題の本質的な難しさは、ビュー定義が単射ではないため一つのビューの更新に対して、基底表に対する更新が複数もしくはそもそも存在しないという点にある。
近年、プログラミング言語分野で広く研究されてきた双方向変換の枠組みに基づき、本課題に取り組む研究が進展している。双方向変換は、更新の望ましい振る舞い(well-behavedness)、すなわち副作用のない意味的整合性を保証する理論的基盤を提供するが、そのまま実用的なデータベースシステムへ適用するには課題が残っている。特に、双方向変換が仮定するビューは、永続的なデータベースオブジェクトではなく、独立したメモリ内構造として扱われる点が、現実のデータベース環境とは乖離している。
実際のデータベースアプリケーションにおいては、ビューと基底表は明示的に区別することなく利用され、データの変更は標準的なSQL文（INSERT, DELETE, UPDATE)を通じて行われる。このため、同様の手法を用いてビューを更新することは、実運用上きわめて重要である。
本研究では、SQLによるビュー更新操作を、well-behavednessを保ったかたちで基底表への更新へと変換する手法を提案する。これにより、理論的な双方向変換の枠組みと現実的なデータベース実装との間のギャップを埋めることを目的とする。

情報システムの多様化に伴い関係データベースと非関係データベースの相互運用やデータ共有の需要が高まっており、異種データ間の一貫性の確保は重要な課題である。関係データモデルとそれ以外では、データベースにおいてアクセス方式が大きく異なるため、従来手法では変換が複雑化しやすい。
双方向変換を用いることで、プログラマが記述する変換を一つに抑えられるが、データサイズが増えるにつれ効率化は喫緊の課題となる。
一方で、データベースは固有のコンパクトなバイナリダンプ形式を持っており、その形式間で双方向変換を行うことで効率化が期待できる。
本研究では、双方向変換言語BiGULを用いた関係-NoSQLデータモデル間の、バイナ形式を媒体とする双方向変換手法を提案する。バイナリファイルからデータ要素を読み込み、バイナリデータ型を操作し、新たなバイナリファイルに結果を書き出す。
バイナリ形式が豊富に持つデータ片の長さ情報を用いた効率的変換が特徴であり、評価により、同期シナリオの一部において性能を向上させることが示された。

This paper proposes an algorithm based on Partial Order Reduction (POR) for a simulator capable of modeling real-scale intra-regional medium-lot cargo transportation (IRMLCT) using the Ambient Calculus (AC). AC is a process algebra used to model and verify the characteristics of concurrent computational processes with dynamically changing hierarchical structures through algebraic expressions. Leveraging this feature, we are researching a system that simulates cargo delivery routes, aiming to improve the loading efficiency of truck transportation. However, attempting to cover all delivery patterns through simulation inevitably leads to the problem of combinatorial explosion. In our previous research, we proposed an algorithm incorporating POR to address this issue, but it proved insufficiently effective for handling real-scale logistics. Furthermore, the method for generating the ample set, which is key to POR, was inadequate and could potentially overlook important delivery patterns. To address this challenge, this paper proposes an improved algorithm designed to further mitigate state space explosion. This is achieved by subdividing the delivery areas of IRMLCT, thereby eliminating the interleaving of mutually unrelated transitions as much as possible while ensuring that important delivery patterns are not overlooked. To this end, this paper also formalizes HTLAC, a language that extends AC to specialize in modeling IRMLCT, and formalizes ALTL_X, a linear temporal logic based on Ambient Logic, the modal logic for AC.

我々が提唱中の並列実行モデルHOPEは「完全冗長実行からの階層的計算省略」に基づく．各HOPEワーカは，分割統治の全範囲をあらかじめ計画した異なる順序で逐次実行しつつ，実行時に他のワーカから結果を得た部分の計算を省略し，全体として障害耐性も並列効率も高める．しかし，計算全体を冗長実行する際に計算に用いるデータを冗長に扱うままでは，ワーカ数を増やすとそれに比例するメモリ容量を要するだけでなく，同じ並列実行時間で扱える問題規模をデータ量としても大きくするなら，それにも比例するメモリ容量を要する．本研究では，大規模行列積を例題として，大容量データをファイルに保持し，メモリにはデータの一部のみを保持するout-of-coreアルゴリズムがこの問題の解決に有効であるかを検討する．

近年，デバイス上で推論を行うエッジAIが注目されている．
ディープラーニング (以下DL) の推論をデバイス上で行うことで，リアルタイム処理が可能となり，通信コストや通信に伴うセキュリティリスクを軽減できる一方，計算資源が小規模のため，高速な推論が課題となる．本研究では，小型デバイスであるRaspberry Piが備える内蔵GPU VideoCore IVに注目する．VideoCore IVは，DL演算のための汎用的な処理を行う機能が十分にあり，CPUを上回る性能を持つことから，DLの推論を高速化できると考えられる．しかし，活用例は少なく，OpenCLのような高水準な並列処理ライブラリのサポートは限定的である．そこで，本研究ではDLモデルのResNet18とYOLOv5nを対象に，推論過程で用いられる主要なDL演算をVideoCore IV向けに実装した．

特定の領域における処理を記述することに特化した領域特化言語（DSL）の構築方法の 1 つに，汎用プログラミング言語の構文を基盤とする埋め込み領域特化言語（EDSL）がある．EDSL では，基盤となる汎用プログラミング言語（親言語）の機能を活用することが可能だが，EDSL の各プログラムの目的や用途を考慮すると，親言語の全機能まで必要とすることはなく，一部の機能は本質的に不要である．ところが，親言語の全機能を利用可能とすると，EDSL に必要以上の機能が提供されるだけでなく，利用者の意図しないプログラムを実行してしまう恐れがある．汎用プログラミング言語の多くの機能は標準ライブラリによって提供されることを考慮し，本論文は，個々の EDSL の目的に応じて親言語のライブラリ利用を制限する制御機構を提案する．我々は親言語を Haskell とする場合と Python とする場合との 2 つのEDSL に対して提案する制御機構を実装し，提案する制御機構の有用性と汎用性を確認した．

領域特化言語 (DSL) の実装方式として，埋め込み領域特化言語 (EDSL) がある．これは既存の汎用言語を基盤 (親言語) とし，そのライブラリとして構築するDSLである．実装の容易さ，既存ツールの再利用性といった利点を備え，設定ファイルとしての活用例も多い．
しかし，特定の目的に特化するDSLと，それを前提としない汎用言語との共存は不整合をもたらす．親言語の組込ライブラリにEDSLの目的外の機能が含まれる場合は多い．この余分な機能の存在により，たとえばEDSLプログラムを設定ファイルとして読み込むだけでも，利用者は任意コード実行のリスクを負う必要がある．
このような問題に対処するため、我々はEDSL中で利用可能な機能を制限する言語独立な設計を提案する．本機構では許可リスト方式によって利用可能な機能を制限し，その迂回をプロセス分離によって防ぐ．我々はプロトタイプをRuby上に実装し，実効性を評価した．

近年，CPUの計算速度とメモリアクセス速度の乖離が性能上のボトルネックになっている．これを克服するため，メモリの近くで計算をするProcessing-in-Memory (PIM)アプローチが注目されている．本研究では，PIMの実装の一つであるUPMEMで，CPUからオフロードされたJavaのメソッドを実行する機構を開発する．UPMEMはDRAMの近くに小規模なプロセッサであるDPUを備えている．本研究では，オフロードするJavaメソッドだけをDPUの機械語にコンパイルする．DPUのプログラムメモリは24KBしかないため，複数のバイナリを入れ替えながら実行する．また，DPUが持つハードウェアスレッドを利用してSPMD方式の並列プログラミングをサポートする．

近年、ソフトウェア開発へのAIエージェントの導入が加速している。AIエージェントは人間に代わり複雑な処理を行える一方で、その生成コードは一般に分量が多く、構造も複雑であるため、ユーザー要件を満たしているかを人手で検証することは容易ではない。この課題は、AIエージェントを実運用に導入する際の大きなボトルネックとなる可能性がある。本研究では、AIエージェントが生成したコードがユーザー要件をどの程度満たしているかを評価する手法の確立を目的とする。具体的には、自然言語タスクにおける評価フレームワークとして近年注目される RAGAs（Retrieval-Augmented Generation Assessment）に着目し、その評価指標をコード生成タスクに応用することを試みた。RAGAsの評価指標の導入により、生成物と参照情報の整合性や回答の妥当性を定量的に評価する枠組みをコード領域にも適用できる可能性が示唆された。しかしその一方で、コード生成タスク特有の性質を RAGAsの指標だけでは十分に捉えきれないという限界も明らかとなった。本発表では、RAGAsの適用可能性と限界を整理するとともに、コード生成タスクの評価に特化した拡張指標の必要性について議論し、今後の評価手法設計に向けた展望を示す。

現在、生成AIの台頭とソフトウェア開発への爆発的な普及を受けて、プログラミング教育において生成AIという新たな道具の活用法をどのように教えるかが大きな課題となっている。本研究では、生成AI利用を前提として課題に取り組んだ学生を対象に、生成AIに与える指示(プロンプト)の書き方とその生成されたプログラムの品質の関係性について調査を行った。調査対象は、名前姓名判断 (初級プログラミング)、機械学習モデル (データサイエンス)、さらにオセロAI(応用プログラミング) である。いずれの場合も体系的な生成AIとプロンプト教育は必要であるが、我々が想定するプロンプト品質 (良いプロンプトの書き方) とプログラムの品質の間には有意な関係性がみられなかった。この結果は、生成AIの活用法として「プロンプト技能」を重視する教育に疑問を投げかけるものである。

The codegen plugin for Coq performs verified compilation from Gallina to C.
As an intermediate step, it transforms Gallina terms into a restricted
subset of Gallina that is structurally closer to C.
For each transformation, codegen automatically generates a proof that the
transformed function is extensionally equal to the original one, i.e.
∀ args, f args = f’ args.

Some transformations are not preserved by Coq’s definitional equality and
therefore cannot be justified by simple computation.
One such case is distributing function applications over match expressions,
which transforms
(match e with C1 ⇒ t1 | … | Cn ⇒ tn end) args
into
match e with C1 ⇒ t1 args | … | Cn ⇒ tn args end.

To prove the semantic preservation of transformations involving recursion,
codegen constructs proof terms that mirror the structure of the original
recursive functions.
This approach supports recursive structures that cannot be handled by Coq’s
standard induction principles such as nat_ind, including mutually recursive
and nested fixpoint functions.
Because the generated proofs share the same recursive structure as the
original functions, they are accepted by Coq’s termination checker without
additional annotations.

This method enables codegen to automatically produce verified semantic
preservation proofs even for complex Gallina-to-Gallina transformations,
providing a solid formal foundation for subsequent verified compilation
to C.

The reference implementation of Ruby (CRuby) requires developers of the interpreter and its C extensions to explicitly call the garbage-collection guard macro (RB_GC_GUARD) when needed to prevent accidental memory reclamation. Omitting this guard can cause interpreter crashes or data corruption. Adding excessive guards can impact runtime performance. In practice, many omissions have been discovered in CRuby.

This paper presents GuardLint, a static analyzer designed to detect omissions of RB_GC_GUARD. It is implemented as CodeQL queries and applied to CRuby’s codebase. The analysis identified 32 guards in the current implementation as necessary. Through careful review of potential omitted and excessive guards, we confirmed one highly likely omission and at least three potential excesses.