2016-05-30追記 Agda2.5.1は割と素直にインストールできるようになりました。先週うまくいかないと書いていたAgda新バージョンのインストールの話。改めて同僚Tさん*1にエラーについて聞いてみたら、原因が判明し、そしてインストールもできたので以下展開。…

最近の修正で、ロケールをなおす必要はなくなって、普通に cabal install agda -f -cpphs と同僚Tさんから聞いてやってみたのだが、失敗。以下ログ。またあとでやってみる。cabalが古いかも。 C:\Windows\system32>cabal install agda -f -cpphs Resolving d…

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.WindowsNotes-2-4-2 きのう同僚Tさんから聞いて驚いたのだが、一度ロケールを英語にしないとインストールできないというcabalのバグ？らしい。すごいな。自分のバージョンはまだ2.3.2だった。

この2週間ぐらい、働いていた時代に自分が作っていたソフトウェアの定式化、みたいなことを考えていた。かなり新しいことを考えたと思ってたけれども、そのうちの一部分は（たぶん）David Spivakがすでにやっている仕事にかなり近い、と思った。 http://d.ha…

本日Agda-MLに流れてきた話によると、Aaron Stumpさんという型方*1がAgda本を執筆中で、出版社とも交渉中とのこと。現在のドラフト版が https://svn.divms.uiowa.edu/repos/clc/projects/agda/book/ にあります。興味がある方はご一読を。ドラフトを15年春ま…

全然違うことを勉強していたら何故かAlgebraとCoalgebraについて知りたくなり、前から積読になっている本Universal Algebra for Computer Scientists (Monographs in Theoretical Computer Science. An EATCS Series)作者: Wolfgang Wechler出版社/メーカー:…

そのAgdaのインストール問題とは別に、Windows7上のVMware playerで動かしているXubuntuが、たぶんWindows7自体をスリープして復帰するときとかにクラッシュする、という問題もあり、これも調べないといかん。うーん。こういうn時間問題（nは不明）は大変。…

Ubuntu（正確にはXubuntu14.02）にAgda2.4.2をインストールしようとして（cabal install agda）、なんかHaskellのあたりでうまくいかなくて困った。が、 http://stackoverflow.com/questions/25104367/ghc-incompatibility-installing-haskell-src-exts-via-…

http://drops.dagstuhl.de/opus/volltexte/2013/3898/pdf/4.pdf http://static.googleusercontent.com/media/research.google.com/ja//pubs/archive/40678.pdf 結局ワールドというのはモデル図にもなるという話なのか、なんかすごいな。あとでちゃんと読むが…

とりあえず、LuaLaTeX上でLuaTeX-jaパッケージを動かして、日本語表示とunicodeのマニアックな記号表示を両立されるところまではできたぞ。環境はWindows7上のTeXWorks。 成果物はGithubに https://github.com/kino3/luatex-ja フォントの制御はまだうまくで…

今日から1日3コマ×3週間でAgdaを使った定理証明実習という講義がはじまる。ぼくはTAとして参加予定で現在インストール手順など作っています。思ったこと。 やっぱり日本語文献を書かねば・・・ WebでAgdaができる環境があればインストールしなくてもいいのに…

お久しぶりです。大学の近くに引っ越して、段ボールの山と格闘しつつ研究を始めています。とりあえずAgda含む日本語論文を書く環境を何とかしようと思い、LuaTeX-jaをごにょごにょしようと思っていたのですが、冷静に考えてみるとTeXの何がどう動いているの…

http://d.hatena.ne.jp/kiiiino3/20140730/1406751992 でも書いたとおり、ドイツに行かなかった代わりにまとまった読書をしようと思い。Category Theory (Oxford Logic Guides)作者: Steve Awodey出版社/メーカー: Oxford University Press, U.S.A.発売日: 2…

http://siguniang.wordpress.com/2013/05/12/dash-is-not-bash/ ubuntuはshebangがshだとbashにならないのね、参考になりました。

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/ぼちぼち更新…

ああそうか、修論提出からここには何も書いてなかったのですね。 何だか最近は、申請書ばかり書いてはいるのですが、３月以降いろいろと刺激を受けて、ようやく自分のやりたいことがきちんと定まってきた感があって充実しています。来週学振の書類出したあた…

なんとか修士論文提出までこぎつけた。明日印刷して17時締切で提出。17日にプレゼン。いろいろと自分の至らないところがわかったこの１か月だった。 また、この１か月でわずかながら進歩を実感した。 そういったものの成果のWebへの吐き出しは、しばらくして…

いろいろとドタバタしそうですが、まじめにこつこつと。