Agdaをさわりはじめてかれこれ2年ぐらいになる。最近ようやく、Agdaの面白さがわかってきて、それを広めたいという気持ちになってきたのでこうしていろいろ書いている。Agdaについてまとまった日本語の情報はあまりに少なく、まとまった日本語の情報がないと…

Agdaではじめてコンパイルしてみたので、そのやり方メモ。環境はWindows7。 emacs上でコードを書く module HelloAgdaWorld where open import IO.Primitive open import Foreign.Haskell open import Data.String main : IO Unit main = putStrLn (toCostrin…

数学する精神―正しさの創造、美しさの発見 (中公新書 1912)作者: 加藤文元出版社/メーカー: 中央公論新社発売日: 2007/09/01メディア: 新書購入: 3人 クリック: 61回この商品を含むブログ (26件) を見る読んだ。2年前に買ったままずっと積読*1になっていたが…

http://www.kino3.jp/ を研究者としての自己紹介サイトにして、いままでのんはちょっとヨコによけました。ちょっとこういうのを作るだけでもいろんな流儀があるみたいで大変疲れます・・・。英語間違ってたらごめんなさい、日本語間違ってたらもっとごめんな…

構成的型理論についての代表著作「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/ぼちぼち更新…