Workshop on Metaprogramming and Related Topics 2025

2025年6月18-19日
お茶の水女子大学理学部3号館 [道順, 地図No.10]

workshop home
段階的計算体系の理論と構築に関するワークショップを 開催します． 今年は，メタプログラミングに関する話題以外に幅広く プログラム言語の理論と実装に関する話題を集めて討論します．

このワークショップは、 科研費 基盤研究(B) 23K24819(代表者 亀山幸義)のサポートを受けています。

プログラム

1日目: 2025年 6月18日 (水)

13:00-13:10 Opening

亀山 幸義 (筑波大学)

13:10-14:30 Session 1: Program Derivation

Folding Heighway Dragon Curves, Shin-Cheng Mu (Academia Sinica), 40+10
The Heighway Dragon is one of the most known fractal curves. There are two ways to construct the curve: repeatedly make a copy of the current curve, rotate it by 90 degrees, and connect them; or repeatedly replace each straight segment in the curve by two segments with a right angle. A natural question is how do we know the two approaches are equivalent?
We represent a dragon curve by a list, and generalize the construction of the curve to allow rotations to both sides. It turns out that the two approaches are respectively a "fold-right" and a "fold-left", and the task is to show that the two folds are equivalent.
Bio: Shin-Cheng Mu, Research Fellow in Academia Sinica, Taiwan.

Decompiler Assistants: Supplementing Traditional Decompilers with Dependent Type Theory and Interactive Decompilation, Danel Batyrbek (University of Tsukuba), 20+10
Decompilation is a crucial step in security analysis and reverse engineering, yet it produces underwhelming results, when compared to its traditional counterpart of compilation. Since complete decompilation is an undecidable process, automatically producing correct decompilation, while preserving correctness, is highly improbable. However, reverse engineers have shown capabilities to recover high-level code that produces identical assembly code as the target program.
Calculus of Inductive Constructs has demonstrated remarkable results in propositional logic and proof assistance, namely, verifying the correctness of proposed proofs. Many proof assistants have desired properties, that are useful in decompilation: rewriting terms, ensuring consistency and constructing tactics. Those properties become crucial with increased scope and/or heavily obfuscated and self-modifying code machine code, which are typical use-cases of decompilation.
My goal for PhD program is to extend modern decompilers with the dependent types and propositional logic to improve correctness and quality of decompiled code.

14:40-17:00 Session 2: Effects

control/promptの CPS変換, 浦中 花菜(お茶の水女子大学), 30+10
従来のcontrol/promptのCPS変換は継続とトレイルを受け取る形で書かれてい る。しかし、それでは正当性の証明がとても複雑になってしまう。トレイルの みを受け取る形にしたCPS変換について考えたので、紹介する。

Towards Programming with Effect Handlers and Typed Holes, Zhiqi Chen (Institute of Science Tokyo), 30+10
Effect handlers are being introduced into many programming languages, but their steep learning curve limits their accessibility to a broader audience. To address this issue, we propose a programming environment in which one can evaluate programs with effect handlers and typed holes. So far, we have developed a novel operational semantics and a type-and-effect system for incomplete effectful programs, as well as a prototype implementation.

A Design Recipe for Algebraic Effects and Handlers, 叢悠悠 (東京科学大学), 15+5
代数的エフェクトとハンドラの設計手順は、代数的データ型と関数の設計手順と類似している。この類似性を利用して、Felleisen らのデザインレシピの考え方を代数的エフェクトとハンドラに適用する。

4種類の限定継続演算子の抽象機械における継続実行の効率化に向けて, 石尾 千晶 (お茶の水女子大学),30+10
4種類の限定継続演算子に対する definitional interpreter から、機械的な 変換を通して ZINC Abstract Machine と同様の最適化を行う抽象機械を導出 する。それを通して、限定継続の効率的な実行につなげることを目指す。

17:00-17:30 Discussion

2日目: 2025年 6月19日 (木)

9:30-10:50 Session 3: Staging

Staged Gradual Typing, 亀山幸義 (筑波大学),30+10
MetaMLスタイルの段階的計算は、静的型付け言語に基盤を置いている。 JavaScriptなどの動的型付け言語を対象にした段階的計算を安全に 表現するためにはどうしたらか、という問いに答える第一歩として、 漸進的型付け言語と多段階計算(の最も単純なもの)を融合した体系を 提案する。(矢口紘人との共同研究)

Reconciling the Conflict Between Online and Offline Code Generation, 村瀬 唯斗 (京都大学) ,30+10
多段階計算と一口に言ってもその主な用途が実行時最適化かオフラインコード生成かでプログラミング言語に求められる要件は大きく異なる。こうした背景の下に多様な多段階計算プログラミング言語が提案され、しばしばそれらの方針は対立し混同されてきた。本講演ではこの二つの方向性を調停するようなMetaML的な多段階λ計算を設計する試みを紹介する。特にこの言語の特徴として 1. Refined Environment Classifier の手法をMetaML的な多段階計算の型システムに適用している点、2. 制限された形の Cross-Stage Persistence をサポートしている点、の二つについて論ずる。

11:05-12:35 Session 5: Implementation

A pair of tricks, Oleg Kiselyov (東北大学), 40+10
One way to ascertain the quality of the generated code~-- its performance, hygiene, memory safety, deadlock freedom, etc.~-- is to decorate it with annotations that explicate some aspect of the code: e.g., the count of particular operations, its free variables, the sequence of IO or memory allocation operations, or correctness proof obligations. The annotations are built along with the generated code, and may be used to detect problems like scope extrusion or an imminent deadlock~-- well before the whole program is generated, let alone executed. Annotations are a worthy alternative to fancy types.
Generating code along with annotations is rather straightforward~-- save generating functions or other variable-binding forms. The often used so-called higher-order abstract syntax (HOAS) also suffers from several known problems. Annotating code brings a new one~-- the thrust of a challenge by Olivier Danvy.
The present paper describes a new, simpler and general solution of the challenge~-- actually, of its general form: pairing of HOAS generators, or direct product of algebra-like structures with HOAS operations. The solution also overcomes the hitherto unsolved HOAS problem: latent effects.

トレーシングJITコンパイラは多段階計算を救えるか？、 吉村 友成 (東京科学大学),30+10
本研究では、トレーシングJITコンパイラを用いることで、少ない労力で多段階計算の高速な処理系の構築を目指す。具体的には、ラムダクロージャで表現された中間コードを生成し、さらにトレーシング時の最適化を促す情報を付加することで、トレーシングJITコンパイラによる高品質なコード生成を誘導する方式を提案する。MetaOCamlで記述された多段階計算プログラムを変換してPyPy処理系上で実行し、提案方式の性能を評価する。

13:30-14:50 Session 6: Effect and Staging

microKanren における conjunction の交互実行, 浅井 健一 (お茶の水女子大学), 30+10
microKanren では disjunction の実行はふたつのストリームをマージすると ころで順番を逆にすることで disjunction の両方を少しずつ実行するように なっている。ここでは、実行途中のストリームを非関数化することで、同様の ことを conjunction について行う方法について紹介する。

Compile-time tensor shape checking via staging, 諏訪 敬之 (京都大学), 30+10
テンソル（ベクトルや行列の一般化）を用いた計算では，寸法の不整合がないことを実際のプログラムの実行よりも前に保証できることが望ましい．これに関しては多くの手法が提案されているが，典型的な既存手法では，ソフトウェア開発プロセスへの適用を阻む，以下のいずれかの点での支障がある： (1) “偽陽性の” 型の不整合を生じやすく，その解消に手動の証明などを要するため，将来の拡張やリファクタリングを煩雑化させやすい．(2) SMTソルバなどによる自動証明に依存しているなどして，検査の所要時間が長い，ないし予測困難である．(3) 2の問題を解消するための静的検査と実行時検査を織り交ぜたハイブリッドな手法でも，実行時に失敗する可能性を排除できないほか，実行時検査によるオーバーヘッドを生じるおそれがある．(4) ニューラルネットワークの実装で頻出する，テンソルに対するbroadcastingやreshapingといった複雑な操作をサポートできない．本研究では，一定の制限と引き換えに，ステージングによってこれらの課題をいずれも解消できる言語設計が可能であることを提案する．この体系ではテンソル形状の整合性の検査は型検査ではなくコード生成時のアサーションによって行なわれ，またコードの生成に成功した場合はそのコードを実行しても決して形状の不整合が起きないことを定理として示している．コード生成は主にコンパイル時に実行されることを想定しており，この場合コード生成の失敗は迅速に報告される．また，実行時にしかテンソルの寸法の情報が得られない場合の検査も，不完全だがさしあたり実行時コード生成によってサポートできることも紹介する．

14:50-15:00 Closing

オーガナイザ： 亀山幸義