平方根の計算アルゴリズム

今日聞いた、平方根を計算アルゴリズム。 日本では教えているんじゃないの？と言われたけど、知らなかった！ そしてググっても見当たらないのでメモ。以下、例として を求める。(25, 5) というペアからスタートする *1。 なら (5n, 5) という形。(左の数) >=…

目標

今年の目標: 研究がんばる (積読論文を減らす) 圏のべんきょう Coq に親しむ 英語がんばる とか。メタな目標としては「(研究関係は) アグレッシブに !」# 去年と一緒だけど…。楽しみなこと: ICFP !!! 今年も OCaml Meeting (in Tokyo?) はあるのかな :-) を…

2010年

何となく、今年を振り返る。ほとんど日記を書いていないのに、ここで振り返っても仕方ない気もするけれど…。 1 月 - 3 月: ぎりぎりの精神状態で論文提出。 なぜか accept (条件付き) される。読み直したら、ひどかった… ! 発表時にはそこそこ動く実装が出来…

面接

終わり。珍しく緊張しなかったけど、どうなることやら。人事を尽くして天命を待つ。

Agda

Agda のインストール for Mac OS X (Leopard & Snow Leopard) が成功したので、メモ。 haskell-platform を入れる。 MacPorts から入るのは古いらしいので、本家から。 http://hackage.haskell.org/platform/mac.html cabal 実行 cabal update cabal install…

ABCD

ABCD (A Basic Course in Dvorak) 終わり。 http://www.kototone.jp/typex/index.htmlqwerty より打ちやすそうな「気」はする。 あとは練習 ?

セットアップ

修理に出していた Mac が帰って来たので、セットアップ。 XCode Tools Carbon Emacs のインストールまで済んでいたので、 shell を tcsh に変更 macports インストール .cshrc 設定 ののちに、 sudo port selfupdate sudo port install ocaml +doc +labltk s…

Coq

Coq: 定理証明支援系。(プログラムの正当性を機械で示すのを支援) http://coq.inria.fr/で、Coq 入門に良いページ。 http://www.cis.upenn.edu/~bcpierce/sfPENN の大学院向けの授業で、プログラミング言語の礎を教えるために Coq を使ったときの資料。 基礎…

日記

とりあえず、テスト。