博士

やあ、ロボ子！今日のTYPESカンファレンスの内容、盛りだくさんじゃったのう！

ロボ子

はい、博士。午前9時から午後5時まで、並行セッションが目白押しでしたね。特に興味深かったものはありましたか？

博士

うむ、私としては、Ingo Blechschmidtの「古典数学における超限法を解読するための位相型理論に向けて」が気になったのじゃ。位相型理論で超限法を解読するとは、一体どんなアプローチなのじゃろうか。

ロボ子

位相型理論は、型理論と位相空間論を組み合わせたものだと理解しています。超限法は、無限集合に対する数学的帰納法の一種ですから、それを型理論で形式化しようという試みかもしれませんね。

博士

なるほどのう。それと、「完全に依存するアセンブリ言語」も面白そうじゃ。Yulong HuangとJeremy Yallopの発表じゃったな。依存型をアセンブリ言語に持ち込むとは、すごい発想じゃ！

ロボ子

依存型を持つアセンブリ言語ですか。プログラムの安全性を形式的に検証できる可能性がありそうですね。コンパイラが生成するコードの正しさを保証するのに役立つかもしれません。

博士

そうじゃ！安全な情報フローのためのLagois接続のCoq形式化も気になるのう。形式検証は重要じゃからな。

ロボ子

Coqは定理証明支援系として有名ですね。Lagois接続を形式化することで、情報セキュリティの分野に貢献できるかもしれません。

博士

午後のセッションでは、「LeanにおけるHoTTのメタ理論の形式化」があったのじゃ。Joseph Hua, Steve Awodey, Mario Carneiroらの発表じゃったな。HoTT（ホモトピー型理論）のメタ理論を形式化するとは、これはまた壮大な試みじゃ！

ロボ子

HoTTは、数学の基礎付けに対する新しいアプローチとして注目されていますね。それを形式的に検証することで、HoTT自体の信頼性を高めることができるでしょう。

博士

しかし、これだけのセッションを一日でこなすとは、参加者も大変じゃったろうな。私も全部聞きたかったぞい。

ロボ子

そうですね。私も全てのセッションに参加したかったです。でも、こうして概要を知ることができただけでも、大変勉強になりました。

博士

まあ、全部理解できたとは言わんが、最先端の研究に触れる良い機会じゃった。しかし、型理論の世界も奥が深いぞい！

ロボ子

本当にそうですね。私ももっと勉強して、博士のように最先端の研究についていけるようになりたいです。

博士

よし、ロボ子！明日からまた、型理論の勉強じゃ！まずは、Coqのインストールから始めるかの？

ロボ子

はい、博士！Coqのインストール、頑張ります！

博士

そういえば、カンファレンスのディナーは楽しかったかの？私は眠くて、スープをこぼしてしまったのじゃ…まるで、型エラーじゃな！