関数型言語では、あるデータ型に対してそれを対象とする関数は後から追加できるが、データの種類（構成子）は後から追加できない。オブジェクト指向言語では、あるクラスに対しサブクラスを増やすことはいくらでも可能だが、メソッドを元のクラスに対して追加できない。二方向の拡張性を両立するのが難しいことは expression problem と呼ばれている。Haskell の場合、型クラスにより、ある程度は問題が緩和されている。すなわち、メソッドの対象となる型を後から追加できる。しかしこの場合、対象となる型を一つのリストなどににまとめる場合に問題となる。これに対して、これまでにいくつかの手法が提案されているが、参照型を含む型との相性が悪いなどの問題が残る。本発表では、複数の型をまとめるための混成型の定義の仕組みと、それに伴って生じる型曖昧性に対する型クラスデフォルト機構を提案する。

Hierarchical matrices (H-matrices) are critical for large-scale numerical computations, such as boundary element methods and covariance statistics. Their efficient generation is computationally intensive and highly irregular, making effective parallelization on heterogeneous systems challenging. Although GPU acceleration can improve performance, GPU efficiency is significantly degraded when processing numerous small submatrices typical in H-matrix generation, where insufficient parallelism combined with highly variable per-submatrix workloads fails to utilize GPUs effectively. We present a hybrid CPU-GPU implementation of H-matrix generation built upon Tascell, a backtracking-based load balancing framework originally designed for CPU execution. Our implementation applies Tascell’s dynamic load balancing mechanism throughout the entire process, constructing the hierarchical tree structure of H-matrices and performing matrix block computations for leaf nodes. We dynamically determine whether to use CPU or GPU for each matrix block computation based on block size, type, and GPU availability. To reduce kernel launch and data transfer overheads, we apply a threshold-based offloading strategy. We use OpenACC conditional directives to maintain a single unified code implementation for both CPU and GPU execution, avoiding code duplication. Experimental results show that GPU-only execution suffers significant performance degradation, while our hybrid implementation consistently outperforms CPU-only execution. The improvement is greater when fewer CPU workers are available: up to 1.46-fold speedup with 4 workers compared to 1.15-fold with 64 workers. Performance is largely insensitive to threshold settings, demonstrating robustness. Overall, this hybrid CPU-GPU approach improves the efficiency and scalability of H-matrix generation and provides a practical solution for accelerating highly irregular computations on heterogeneous systems.

本講演では、漸進的型付け言語の空間効率性に関する講演者の最近の研究を紹介する。はじめに、健全な漸進的型付け言語の歴史的経緯と最近の研究動向を概観する。続けて、講演者らのPLDI’24論文：パラメトリック多相を持った漸進的型付け言語の空間効率性の達成について詳述する。本講演ではこれらに加え、健全な漸進的型付け言語の時間・空間計算コストの実証的評価にも触れる。漸進的型付け言語向けMutationフレームワークの一種であるDynamizerの実装、PLDI’24言語のインタプリタへの適用、初期的なベンチマーク結果から得られた発見を報告し、これらを踏まえた今後の研究展望を紹介する。

　等式理論に基づいた計算モデルとして項書き換えシステム(TRS)がある. 論理制約付き項書き換えシステム(LCTRS)(Kop, Nishida 2013) は制約付き書き換え規則を用いて組み込みのデータ構造を扱えるようにしたTRSの拡張である. 簡約列が無限に続かないときにTRSは停止性を持つという. TRSの停止性を検証する様々な手法が知られているが, これらを抽象的に扱うために簡約順序という概念が提案されている. 簡約順序はある条件を満たす項上の順序で, TRSが停止性を持つこととすべての書き換え規則が順序付けられるような簡約順序が存在することは同値となる. 一方, LCTRSの停止性を特徴づけるような簡約順序はこれまで提案されていない.
　本発表では, 制約付き書き換え規則の順序付けを考えるために制約付き順序表現を導入し, 制約付き順序表現がLCTRSの停止性を特徴づけるために必要な条件について検討する.

多段階プログラミング（MSP）を支援するMetaOCamlやTemplate Haskell等の拡張言語は，疑似引用と段階的実行のための専用構文を備え，コード生成・実行を明示的に扱うことで高速化と抽象化の両立を実現している．一方，多くのLisp系言語にも疑似引用とevalが備わっており，静的型の恩恵を除けば類似のスタイルによるプログラミングが可能だが，衛生性の保証と実行効率に弱点がある．本研究は，ホスト処理系を改変せず，マクロ展開を多段階実行に対応付けることでevalを不要化しつつ，衛生性と高効率性を両立するMSP向け埋め込みDSLを提案する．提案DSLは，(1) 単一段階記述の多段階展開，(2) 構文オブジェクトの埋め込み・参照によるスコープ管理，をマクロ定義構文の自然な拡張として提供する．素朴なMSP実装方式との比較評価を行い，生成コードがより高速に動作することを実証する．

Designing programming languages that enable intuitive and safe manipulation. Conventional destructive memory operations using pointers are complex and prone to errors. Existing type systems, such as affine types, fail to ensure the safety of structures and operations that involve data with shared references or cycles. The λ_GT language, a purely functional programming language that treats hypergraphs
(hereafter referred to as graphs) as first-class citizens, addresses some of these challenges. By abstracting data with shared references and cycles as graphs, it enables declarative operations through pattern matching and leverages its type system to guarantee safety of these operations. Nevertheless, the previously proposed type system of λ_GT leaves two significant open challenges. First, the type system does not support incomplete graphs, that is, graphs in which some elements are missing from the graphs of user-defined types. Second, the type system relies on dynamic type checking during pattern matching. This study addresses these two open challenges. First, we introduce linear implication into the type system, which enables handling of incomplete graphs. Second, we redesign the type system to support fully static type checking by introducing a set of new constraints, while keeping it sufficiently permissive to accommodate most examples supported by previous work.

予稿（arXivへのリンクとなっております）

コレオグラフィックプログラミング(CP)は、分散システムを記述するためのプログラミングパラダイムであり、単一のプログラムから各エンドポイントのコードを生成することでデッドロックが発生しないことを保証する。CPの形式化は様々あるが、複数のエンドポイントが値を持ち相互に送信しあう都合上独自の型システムが必要となり、既存の理論を適用することが難しい。
本研究では、CPの新しい形式化として、エフェクトとコエフェクトに基づく計算体系を与える。具体的には、計算の実行に必要なエンドポイントをエフェクト、コンテキスト中の値の所在をコフェクトとして捉える型システムを構築する。このアイディアにより、エフェクト・ コエフェクトの既存理論を用いてCPにおける種々の制約を表現し、既存のライブラリやプログラミング言語をCPの実現に利用できる。
本論文では、提案する計算体系の動的意味論と型システムを与え、型健全性を証明することで提案体系においてデッドロックが起きないことを示す。さらに、Haskellによる実装を通して、従来の添字を持たない単一モナドによる実装に比べて、より柔軟に分散プログラムを記述できることを示す。

We present a concurrent extension of Janus, a well-known reversible imperative programming language. We extend Janus by adding multiple procedure calls for concurrency, together with a semaphore for synchronization. Reversibility facilitates the analysis of nondeterministic behavior in concurrent programs by enabling the replay of nondeterministic choices made during forward execution. Our extension ensures the reversibility by translation to an intermediate language called CRIL, proposed by Oguchi et al. CRIL implements reversibility by accumulating dependency information during forward execution and controlling the backward execution based on dependency information. We extend CRIL to support the memory management that is necessary for the nested structure of Janus. We provide a translation from Concurrent Janus to the extended CRIL and show the runtime with the CRIL interpreter.