Programming in Martin-Löf's Type Theory
構成的型理論についての代表著作「Programming in Martin-Löf's Type Theory」をAgdaで書きながら勉強するgithubリポジトリを作成しました。
https://github.com/kino3/PiMLTT
元論文PDF
http://www.cse.chalmers.se/research/group/logic/book/
ぼちぼち更新していきます。
構成的型理論については日本語の情報が少なすぎると思うので、ぼちぼち書いていきたいと思っています。