2010-08-01から1ヶ月間の記事一覧
8/29 に、Coq庵 に行ってきました。 資料等はこちら。 行き道で祭りやってた。 一部道が通れなかったりして、少し迷うなど。 初めてのCoq 仕様記述言語 Prolog ACL2, HOL/Light 完全自動証明 自動で証明してくれるが、表現力がやや低い Isabelle/HOL, Coq, A…
8/28 に、OCaml Meeting 2010 in Nagoya に行ってきました。 朝早く起きて名古屋大学へ。 暑い・・・ やってみようOCaml / Walk with OCaml OCamlの基礎についてのお話 会場の人の殆どはOCamlでプログラムを書いたことがあるみたい haXeって言語がある Flash…
楚人に盾と矛とを鬻（ひさ）ぐ者有り。之（これ）を誉めて（ほめて）曰く「吾が盾の堅きこと、能く（よく）陥す（とほす）もの莫し（なし）」と。また、その矛をほめていはく、「わが矛の利なること、物において陥（とほ）さざることなきなり。」と。あるひ…
学校の売店に注文してた本が届いたそうなのでもらってきた。 Emacsの本 Emacsテクニックバイブル ?作業効率をカイゼンする200の技?作者: るびきち出版社/メーカー: 技術評論社発売日: 2010/08/03メディア: 単行本（ソフトカバー）購入: 26人 クリック: 1,031…
NotNull型を継承すれば、自分で作った型に関しては、nullが入らないことを静的に保証することができます。 class X extends NotNull { ... } とすると、X型の変数にはnullが入れられません。 http://twitter.com/kmizu/status/21992714816 やってみる。 scal…
Coq りさん Coq りさん、フィボナッチ数列の末尾再帰にしたやつって、本当に元のと同じなんですか？ Fixpoint fib1 (n : nat) : nat := match n with | 0 => 0 | 1 => 1 | S n => fib1 n + fib1 (pred n) end. Fixpoint fib2 (a b n : nat) : nat := match n…
∃a∀b[P(a, b)] → ∀b∃a[P(a, b)] Lemma exists_forall : forall (A:Type)(P: A -> A -> Prop), (exists a:A, forall b:A, P a b) -> (forall b:A, exists a:A, P a b). Proof. intros A P H1 a. elim H1. intros x H2. exists x. apply H2. Qed.
8/21 に、わんくま名古屋勉強会 #14で発表してきました。 OCaml の入門。自分も初心者みたいなもんなんで、勉強しつつです。 今回は10分程余っちゃった。 資料はここに。 OCaml に少しでも興味を持って頂けたら幸いです。 (8/28 に OCaml Meeting 2010 in Na…
8/20 に、第10回名古屋Scala勉強会に参加してきました。 今回は21章と22章。 21章 暗黙の型変換とパラメーター any2stringadd 怖い scala> 1 -> "a" + "b" res0: java.lang.String = (1,a)b null爆発しろ！ implicit parameters、型によって変えられる Monad…
遅くなりましたが、 7/30に、第25回 名古屋アジャイル勉強会に参加してきました。 今回は、「付箋紙ではじめる、いきいきタスク管理！ワークショップ」。 自分はテキストファイルでの管理が中心。 研究室ではタスク看板的なものも作ってみたんだけど、なかな…
