日々の流転

λ. カテ……

圏論勉強会で現在読んでいる“Categories, Types and Structures”について ソフトウェア科学のための論理学 (岩波講座 ソフトウェア科学)(萩谷 昌己) に以下のように書かれていた。カテゴリーの「カテ」までしか書いてないのかよ……

計算機科学者のためのカテゴリー理論の教科書である。計算機科学における応用も含めて、カテゴリーの基礎概念について丁寧に説明している。カテゴリーの「カテ」まで書いてある。残念ながら体裁があまりきれいでない。

λ. “Program-ing Finger Trees in Coq” by Matthieu Sozeau

Finger Tree の実装をダシに、Coqの上に実装されたRusselという言語(?)を紹介している感じ。

しかし、Program-ing Finger Trees In Coq or How To Morph Endo Using Type Theory というスライドのタイトルには笑った。