2004-09-27 [長年日記]
λ. 今日から授業開始。
λ. 東方永夜抄のスペルカード取得率
スペルプラクティスで取得/挑戦可能/総数が199/207/222。残りは6Aの禁薬「蓬莱の薬」のHardとLunatic、6BのLuntatic全部、Extraの「インペリシャブルシューティング」、それに Last Word が半分くらいか……。いまだに「深弾幕結界 -夢幻泡影-」を見れねぇ。
λ. 本宮ひろしと集英社に抗議を!!
ヤングジャンプで連載中の「国が燃える」での南京事件の過激な誇張に抗議しようって話。フィクションとはいえ、私もこの描写はあまりに酷いと思う。
λ. Epigram
Epigram is a dependently typed programming
language and an interactive programming
environment. Epigram has got a type system which is strong
enough to express the behaviour of programs, the type checker
then guarantees that the program is well behaved. However, you
don't have to go as far, you can write ordinary programs
and refactor them into more trustworthy, formally
checked deliverables -- Epigram supports a pay as you go
approach to formal methods.
Epigram is a dependently typed functional programming language.
って事で少し興味をひかれる。誰か使ったことあるひといない?
【2006-04-22 追記】 xemacsが必要なのと、自然演繹のスタイルでプログラムを書かなくてはいけないのが、ちょっと嫌かも。