高位合成（HLS）では再帰の扱いが難しく，再帰で自然に表現されるアルゴリズムを利用者が手作業で反復処理へ書き換える必要がある．本研究では，HLS向け再帰除去をプログラム合成問題として定式化し，再帰プログラムを非再帰または反復的な計算構造へ自動変換する手法を検討する．提案法では，変換先を自由に探索するのではなく，対象プログラムの構造に応じたテンプレートを与え，元プログラムとの入出力整合性に基づいて未知部分を合成する．これにより，線形再帰に対する有限状態表現への変換と，分割統治型再帰に対する木状反復計算への変換を，共通の枠組みで扱うことを目指す．本研究は，再帰の除去そのものだけでなく，ハードウェア実装に適した計算構造への変換を統一的に扱う基盤となることが期待される．

SMTソルバのソルバ選択では，制約式から抽出した静的特徴に基づいて機械学習によりソルバを選択するMachSMTなどの手法が知られている．本研究では，Z3 の tactic 適用結果・probe 値・短時間実行の solver 統計といった Z3 から取得可能な特徴を，問題の構造的性質や求解難易度を反映する情報源として用いる．Z3 は他の SMT ソルバに比べ，外部から取得可能な実行情報が豊富であり，Z3から得られた実行情報を静的特徴に追加することで，ソルバ選択の精度向上が見込まれるかを検討した．Z3 由来の特徴を抽出して MachSMT に統合する評価パイプラインを実装し，QF_BVとQF_NIAとQF_FPのロジックを対象とした分析を行った．特徴群の寄与がロジックによって異なることが示唆されており，本論文ではその要因分析と，結果がサンプル構成に対して不安定になる現象の相関分析による解明と，静的特徴のみからZ3由来特徴を予測する蒸留手法の有効性についても報告する．

LLMは多くのプログラミング言語において高いコード生成能力を示すが、その能力が各言語ごとに獲得されたものか、言語によらず共通する能力なのかは明らかでない。本研究では、事前学習データに含まれないことが保証された新規プログラミング言語 Yuiを設計し、言語仕様やコード例からなる文脈情報を与えた際のコード生成性能を、HumanEval 相当の164間のベンチマーク（YuiEval）を用いて定量的に評価した。実験の結果、適切な文脈情報を付与することで未知言語のコード生成が可能となること、またコード例と自然言語での説明など特性の異なる文脈情報を組み合わせることで、単独の文脈情報を大きく上回る性能が得られることを確認した。これらの結果は、LLMのコード生成能力がアルゴリズムの推論という言語非依存な要素を含み、文脈内学習によって未知言語の構文規則を獲得することで、その能力を新たな言語へ転移できることを示唆する.

ソフトウェア開発では，ユースケース図やシーケンス図などのモデル図が広く利用されている．近年，視覚言語モデル（VLM）をモデル図の理解やコード生成に活用する動きが加速しているが，セキュリティ上の制約により商用 VLM を利用できない開発現場では，ローカル PC 上で動作するオープンソースVLM の活用が現実的な選択肢となっている．本研究では，9 種類のモデル図を対象とした 240 問の 4 択問題からなる評価ベンチマークを構築し，商用 VLM および Apple MLX 上のオープンソース VLM を含む計 17 種類の VLM の理解能力を体系的に調査した．実験の結果，商用 VLM の最高正答率 87.2%に対し，MLX 上の Gemma 4（26B，4bit 量子化）は 71.7%を達成し，Claude Haiku 4.5 の 68.5%を上回ることが明らかになった．また，PowerPoint，PlantUML，ホワイトボード，紙への手描きという 4 種類の描画手段を比較した結果，手描き図であってもデジタル清書を経ずに VLM による理解が可能であることが示された．

情報系学生が学ぶ「離散数学」や「微分積分学」，「アルゴリズムとデータ構造」などの科目では，全称量化子・存在量化子を含む多重量化文として表される定義や命題が繰り返し現れる．たとえば，関数の全射性の定義，数列の収束や関数の極限で現れる，いわゆる ε-N 論法や ε-δ 論法による定義，および，漸近的計算量を表すオーダー記法においては，量化子の順序や依存関係が本質的に現れる．しかし学習者は，量化子の順序の違いや，存在量化された変数が何に依存するのかといった多重量化文の基本的な読み方を理解すること，および，多重量化を含む命題を証明することに，しばしば困難を覚える．本発表では，これらの困難に対する支援を目的として，述語論理式として表された多重量化文の意味，とりわけ量化子の順序や依存関係を可視化する教育用プログラムの可能性を検討する．具体的には，論理学教育における既存研究を概観した上で，形式論理学におけるゲーム意味論に基づく可視化手法の構想を述べる．

Tagless Finalは，型付き埋め込みDSLの実装手法である。本発表では，Lean 4上でTagless Finalにより小さなDSLを記述し，評価，文字列化，部分評価といったインタプリタを実装する。さらに，インタプリタが満たすべき法則をインターフェースとして定式化する。法則を満たす実装を与えることで，具体的なインタプリタに対する証明をTagless Finalの枠組みの上で導けることを示す。これにより，Tagless Finalの抽象化が解釈の追加だけでなく，性質の定義と形式的検証にも有効であることを示す。また，部分評価器の実装を通じて，コード変換に伴う設計上の課題について議論する。

Current quantum computers are primarily used as accelerators that execute certain computations at high speed under the control of classical computers. In our previous work, we generalized this paradigm and investigated a distributed computing architecture consisting of multiple classical nodes, each equipped with a quantum processing unit.
In this paper, we design a high-level programming language suited for such quantum-classical hybrid distributed architectures. The language is founded on a lambda calculus for staged computation originally developed in the context of classical computing, extended with a multi-modal type system that statically distinguishes between classical and quantum computation stages on which computations are executed. This type-theoretic approach enables the programmer to describe heterogeneous distributed quantum-classical programs within a single, coherent framework. We present a prototype interpreter for the language, simulating quantum computation via state vector simulation. Through this implementation, we show that the staged computation paradigm provides a natural and principled foundation for programming quantum-classical hybrid distributed systems.

Complex systems, including scheduling problems which constitute a class of constraint satisfaction problems, are prone to correctness errors. In this presentation, we show a case study of implementing such an inherently complicated system accompanied with machine-checked proofs for its correctness in the programming language Idris.
We consider a scheduling program for university project presentations, which was first implemented in Haskell. To obtain machine-checked correctness, we translate the program to Idris, a dependently typed language, in which types can encode and enforce logical properties of arbitrary complexity, allowing assumptions that were previously informal to be made explicit and checked during compilation.
Currently, we have formally encoded several correctness properties. The fairness condition, which governs how the calculated schedules are partitioned into groups, has been encoded to statically rules out any malformed grouping. The condition under which a fair grouping exists for a given number of presentations has been proven decidable. We also have implemented the core algorithm with correctness proofs of the scheduling program, which is based on a nested application of calculating combinations with filtering from sets (implemented in length-indexed vectors) of several types with several filtering criteria. Remaining challenges include fully implementing the system in Idris but we expect it will be done shortly.

文字列を扱う多くのプログラムでは，ユーザ入力の検証やアクセス制御などの処理において，正規表現マッチングが広く利用されている．しかし，主流であるバックトラック方式の実装は，入力長に対して計算時間が最悪の場合に指数的に増大し，サービス拒否を引き起こすReDoS攻撃の要因となることが知られている．藤浪・蓮尾の先行研究では，計算結果をメモ化して再利用することで重複計算を防ぎ，先読みと後読みで拡張された正規表現に対して線形時間で動作するアルゴリズムが提案されている．本研究では，このアルゴリズムをDafny上で実装し，その自動検証機能を用いてアルゴリズムの正当性と線形時間性を機械的に保証する．

関数型言語Elixir/Erlang等はBEAMと呼ばれる仮想マシンで実行される。このときの実行の単位としてプロセスの概念がある。これはアクターモデルに準じており、独立した互いに疎な軽いプロセス同士が通信する機構を採用することで並列プログラミングを容易にしている。
サービスやシステムを構築する際に、このプロセスの実行をあるBEAMから別のBEAMに移動させたくなることがある。しかしながらBEAM自体にはこの機能は直接実装されてはいない。我々はこの機能をプロセスライブマイグレーションと呼んでおり、これが実現できるとハードウェア資源の変化や広域分散システムでネットワークの特性が変化した場合に、プロセスの適性な配置を実現することが可能になる。
今回はElixirプロセスのライブマイグレーションを実現する方法を提案する。これはElixirプロセスのなかでもGenServerと呼ばれるプロセスに特化し、さらに出版/購読型通信を用いることで実現するものである。出版/購読型通信を用いることで、IP通信が非対称な特性になってしまう広域分散環境においてもマイグレーションの動作を可能にした。

データマイニングの分野において，複数の事例から仮説を生成する帰納論理プログラミング（Inductive Logic Programming, ILP）は，完全に説明可能であり，深層学習ベースのシステムと比べ，構造化データから新しい関係を抽出するために有効であることが知られている．ILPは，一階述語論理に基づいて仮説を生成するので，その過程で生じる多くの演繹のコストが高く，ビッグデータへの適用を難しくしていた．本研究では，メタヒューリスティクスの１つである粒⼦群最適化（Particle Swarm Optimization，PSO）を用いて，ILP システムの仮説探索を高速化する手法を提案する．本ILPシステムは，先行研究で示したプロトタイプを，組合せ型と経路探索型の2種類の粒子表現を基に実践的なシステムとして実現しており，それぞれの粒子表現方法を示すとともに，その影響を，既存のILPシステムと比較しながら，実験評価をとおして示す．