我々の分野の国際会議紹介

目的

近年、LLMの急速な発展に伴い、vibe codingなどで実装されたソフトウェアの妥当性・安全性を保証するために、形式検証・プログラム検証（Leanなど）の重要性はかつてないほど高まっています。しかし、これらに関連する研究者たちが活躍している主要なコミュニティについては、分野外の方々にはなかなか実情がわかりにくい状況にあると考えます。本記事では、これらに関連するプログラミング言語・理論計算機科学（論理）・形式検証の三領域にまたがって主要な国際会議を紹介します。¹²

ちなみにプログラミング言語・理論計算機科学（論理）・形式検証における日本の研究者の国際的プレゼンスは十分に高く、例えばCSRankingsに基づくと、教員数は多くないものの、アジアの他の大学と比べて遜色ないスコアとなっています。

前置き

本記事は所属組織を代表するものではなく、あくまで個人的見解に基づいたものです。

Core rankingやCSRankingsなどの既存のランキングもありますが、最終的に当該分野の研究者の肌感覚によってしか判断できないと考えるので、分野外の方々向けにプログラミング言語・理論計算機科学（論理）・形式検証などに関連する主要な国際会議を列挙します。

プレミア国際会議

プログラミング言語

• PLDI プログラミング言語の設計と実装を扱う代表的な国際会議です。コンパイラ最適化などの言語実装、メモリ管理などの実行時システム、プログラムの静的・動的解析を伝統的に扱っており、形式検証も継続的なテーマです。実装や実証的評価から得られる知見を重視します。³

• POPL プログラミング言語の基礎原理を扱う代表的な国際会議です。主なトピックには、プログラム検証、型理論、プログラム解析などがあります。論理的・数学的な研究に特に強く、提案する手法に対する形式的・数学的な裏付けを重視します。

理論計算機科学（論理）

• LICS 理論計算機科学における論理分野を代表する国際会議です。数理論理に加え、型理論、意味論、オートマトン、形式検証、並行・確率システム、有限モデル理論、計算量理論など、幅広い分野を対象とします。理論の面白さが重視されます。

形式検証

• CAV 形式検証分野を代表する会議です。主なトピックには、モデル検査、SAT/SMT、実行時検証、システム検証、定理証明支援系などが含まれています。実世界のソフトウェア・ハードウェアなどに対する実用的な検証手法の開発を目指した理論・アルゴリズム・ツールなどを扱います。

トップ国際会議

プログラミング言語

• OOPSLA 名称の”OO”はオブジェクト指向に由来しますが、現在はオブジェクト指向との関連を問わず、プログラミング言語とソフトウェア工学を広く対象とする国際会議です。言語設計やプログラム解析・検証から、開発環境やプログラミングの実践に関する研究まで扱っています。研究テーマ・研究方法ともに、分野の主流から外れる研究も歓迎する懐の広い会議です。

• ICFP 関数型プログラミング分野を代表する国際会議です。ラムダ計算、型システム、意味論などの基礎理論から、言語設計、処理系まで幅広く扱います。また、プログラミング上のアイデアや技法を紹介するFunctional Pearlや、実際のシステム開発・運用から得られた知見を報告するExperience Reportなど、特色ある論文カテゴリを設けています。

• ESOP ICFPなどの特定の領域に特化した会議を除くと、POPLに次ぐプログラミング言語理論の代表的国際会議です。 採択されるトピックはPOPLとほぼ同様で、OOPSLAに比べると理論色が強いです。

理論計算機科学（論理）

• ICALP（Track B） トラックA（Algorithms, Complexity and Games）とトラックB（Automata, Logic, Semantics, and Theory of Programming）の二つからなり、とくにトラックBはこの分野を代表する国際会議の一つです。計算の形式モデルと意味論を幅広く扱います。ICALP 2027から2ラウンド制になり、LICSと投稿期間が重ならない形での投稿が可能になりました。

• FoSSaCS LICSに次ぐ理論計算機科学（論理）の主要会議です。論理、オートマトン、検証、型理論など幅広いトピックを扱っています。LICSと比較するとややプログラムや遷移システムの意味論に関する論文が多い印象があります。

• CONCUR 並行性理論を専門とする、状態遷移系やオートマトンに関する理論計算機科学の会議です。伝統的には並行性に関するプロセス代数や双模倣性などが主流ですが、近年は名前ほど並行性に限定されておらず、状態遷移系とその振る舞いに関する基礎理論を広く扱います。

• FSCD 計算と演繹の理論的基礎を扱う代表的な国際会議です。項書換え、ラムダ計算、証明論、型理論を中心に、自動推論、意味論、形式検証などを扱います。

形式検証

• TACAS CAVに次ぐ形式検証の代表的国際会議です。採択されるトピックはCAVとほぼ同様ですが、やや理論色が強いことが多いです。

• IJCAR 隔年で開催される、CADE、FroCoS、TABLEAUXの3会議による合同国際会議です。自動推論・定理証明を中心に、SAT/SMTや項書換え、決定手続き、推論手法の組み合わせ・統合、証明論、Leanなどの定理証明支援系に関する研究を幅広く扱います。

形式検証に関連する論文がよく通るトップ国際会議

形式検証に関する論文は、例えば以下のような、関連する周辺分野の国際会議にもしばしば採択されています。

• EMSOFT 組込みソフトウェアに関するプレミア国際会議です。採択論文は隔年でIEEE TCADかACM TECSに掲載されます。形式検証もスコープに入っており、形式検証に関連する論文が例年採択されています。

• AAAI + IJCAI AI分野のプレミア国際会議です。伝統的に論理・形式手法・モデル検査の論文が毎年一定数採択されています。確率的システムの形式検証・安全な強化学習・時相論理などに関する論文が多いです。

文責：郡 茉友子、酒寄 健、田邉 裕大、中村 誠希、和賀 正樹、渡邉 知樹（五十音順）

---

1. 日本では、これらの三領域にまたがって活躍する研究者が珍しくありませんが、世界的にはこれらの三分野は隣接する異なる分野と見なされています。実際に、このうちの一つの分野にのみ論文を投稿する一流の研究者も珍しくありません。↩︎

2. 一般に論文の出版形態には国際会議とジャーナル（論文誌）がありますが、計算機科学ではジャーナルよりも国際会議の方が主戦場とされる場合がよくあります。↩︎

3. PLDIおよび以下で紹介するPOPL, OOPSLA, ICFPの論文は会議プロシーディングスではなく、Proceedings of the ACM on Programming Languages（PACMPL）という査読付き学術雑誌の論文として出版されます。↩︎