2010-01-01から1年間の記事一覧

NGK忘年会2010

12/ 4 に、NGK忘年会2010 に参加してきました。 UST http://www.ustream.tv/recorded/11239442 ラーメン食ったり、Mac見てたりして少し遅れた・・・ メモ取れたところから。 イベント・コミュニティの話 勉強したいことがあったら勉強会をひらいてみる 続け…

Coq Party

11/27 に、Coq Partyに参加してきました。 資料などはこちら。 エンジニア・ミーツ・Coq すぐ分かる形式手法 形式手法とは? 品質の高いソフトウェアを作るための科学的な仕様記述・検証手法 仕様化の正しさは終盤のシステムテストまで分からない 結合テスト…

けんろん!〜休日カフェタイム〜 第2話演習!

11/21 に、けんろん!〜休日カフェタイム〜 第2話演習! に参加してきました。 USTREAM 第1話 http://www.ustream.tv/recorded/10255923 (前半) http://www.ustream.tv/recorded/10256470 (後半) 第2話 http://www.ustream.tv/recorded/10995206 (前半) http…

第13回名古屋Scala

11/19 に、第13回名古屋Scala勉強会に参加してきました。 27章 オブジェクトを使ったモジュラープログラミング モジュールとしてオブジェクトを捉える Lift とかそうなってる OCaml の(ファーストクラス)モジュールに近い 継承とかも出来る DI 結構普通、そ…

GitとGitHubを体験しながら身につける勉強会 第2回

10/30 に、GitとGitHubを体験しながら身につける勉強会 第2回 に参加してきました。 始まる前に、bleis と F# の GUI まわりって Functional ちっくに書けたりするっぽいねとか、 そういうことは osiire さんが詳しいよとか話してたら、なんとご本人登場。 …

Boost.勉強会 #3 関西

10/23に、Boost.勉強会 #3 関西に行ってきました。 千里中央駅からが分かりにくい・・・>< 10時ちょっと過ぎに到着・・・ まとめかメモかなんかそういう 発表資料が遅延評価されたらしく、順番が少し前後 「C++かわいい。」 OAuth めんどいらしい D はとて…

Jaav っぽいの

なんか bleis 先生が関数型っぽいライブラリを Java で作ってるっぽくて、自分も作ってみようかなーって適当に作ってたらとても残念な感じになったのでのっけてみる。 コードは rf0444's jaav at master - GitHub に。 よくもこんなキチ(ry まずは Function …

わんくま名古屋勉強会#15

10/16 に、わんくま名古屋勉強会 #15に参加してきました。 C++かわいい。λかわいい。 VBにパターンマッチはないらしい。(C++にもない?) 懇親会で、bleis 先生が Java で Jaav っていうライブラリ作ってるって言ってた。 (パターンマッチは少しあるらしい)

第12回名古屋Scala

10/15 に、第12回名古屋Scala勉強会に参加してきました。 24章 抽出子 Haskell に View Pattern ってのがある リスト 24.1 これはひどい Scalaである意味がない。split後なにやってるか分からない パターンマッチ素敵 なにやってるかとてもよく分かる => (Sc…

名古屋Hackathon

10/9に名古屋Hackathon - ラムダ村に参加しました。 自分は Coq 組で参加。Coq to Scala をやってた。 Coq 組の朝は遅い。にわとりなのに。 環境構築に時間かかってた。make 長い・・・ 最初は Scheme や Haskell のを修正していく感じだったけど、読むだけ…

reflexivityつおい

Require Import List. Theorem sum_10_eq_55 : fold_left (fun y x => y + x) (seq 1 10) 0 = 55. Proof. reflexivity. Qed.ぅゎ、reflexivity っぉぃ。

練習リポ

Coq で練習してたファイルたちを github で管理。 rf0444's coq

GitとGitHubを体験しながら身につける勉強会

9/18 に、GitとGitHubを体験しながら身につける勉強会に参加してきました。 USBメモリにぶち込んだ Ubuntu の初実践(?)。 merge とか使わない。rebase 使う。 (by bleis) .bashrc の PS1 に $(__git_ps) で現在のブランチを表示できる 自分の .bashrc もこん…

第11回名古屋Scala

9/17 に、第11回名古屋Scala勉強会に参加してきました。 今回は23章と24章の予定だったけど、盛り上がったので24章は次回に。 23章 for 式の再説 モナド (1) bind : M[A] => (A => M[B]) => M[B] 最初の M[A] がレシーバ (Scala) return : A => M[A] この 2 …

続・Coqりさん Q.E.D.

Coqりさん 証明のかけら の続き (再挑戦)。 Require Import Arith. Fixpoint fib1 n:nat := match n with | 0 => 0 | 1 => 1 | S (S m as p) => fib1 p + fib1 m end. Fixpoint fib2 n a b:nat := match n with | 0 => a | S n => fib2 n b (a + b) end. Lem…

SKK とか

K I = F と、S K K = I を証明してみる。 Definition I {A:Type} x:A := x. Definition K {A B:Type} (x:A) (y:B) := x. Definition F {A B:Type} (x:A) (y:B) := y. Definition S {A B C:Type} (x:A->B->C) (y:A->B) (z:A) := x z (y z). Theorem ki_f : fo…

第1回 Scala座

9/4 に、第1回 Scala座に行ってきました。 資料などはこちら。Ustream はこちら。 開会の挨拶 Scala座 全国レベルのScalaの勉強会! 大きなイベントは関東が多い 悔しい! → 名古屋で開催! これまでのScala、これからのScala これまで編 Scalaって JVM上で…

|> in Scala

F# の |> を Scala でやってみた。 scala> class Holder[A](a:A) { | def |>[B](f:A => B) = f(a) | } defined class Holder scala> implicit def any2holder[A](a:A) = new Holder(a) any2holder: [A](a: A)Holder[A] scala> val succ = (x:Int) => x + 1 s…

メモ晒し

Coq

自分の Coq メモを晒してみる。 ■ ; について T1 ; T2 T1 適用後、T1 によって出来た全てのサブゴールに対して T2 を適用 T1 ; [T2 | T3] T1 適用後、T1 によって出来たサブゴール a, b に対して、a に T2、b に T3 を適用 (不要なら T2, T3 を省略可(何もし…

Coq庵

8/29 に、Coq庵 に行ってきました。 資料等はこちら。 行き道で祭りやってた。 一部道が通れなかったりして、少し迷うなど。 初めてのCoq 仕様記述言語 Prolog ACL2, HOL/Light 完全自動証明 自動で証明してくれるが、表現力がやや低い Isabelle/HOL, Coq, A…

OCaml Meeting 2010 in Nagoya

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

NotNull型を継承すれば、自分で作った型に関しては、nullが入らないことを静的に保証することができます。 class X extends NotNull { ... } とすると、X型の変数にはnullが入れられません。 http://twitter.com/kmizu/status/21992714816 やってみる。 scal…

Coqりさん 証明のかけら

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.

わんくま名古屋勉強会#14

8/21 に、わんくま名古屋勉強会 #14で発表してきました。 OCaml の入門。自分も初心者みたいなもんなんで、勉強しつつです。 今回は10分程余っちゃった。 資料はここに。 OCaml に少しでも興味を持って頂けたら幸いです。 (8/28 に OCaml Meeting 2010 in Na…

第10回名古屋Scala

8/20 に、第10回名古屋Scala勉強会に参加してきました。 今回は21章と22章。 21章 暗黙の型変換とパラメーター any2stringadd 怖い scala> 1 -> "a" + "b" res0: java.lang.String = (1,a)b null爆発しろ! implicit parameters、型によって変えられる Monad…

第25回名古屋アジャイル勉強会

遅くなりましたが、 7/30に、第25回 名古屋アジャイル勉強会に参加してきました。 今回は、「付箋紙ではじめる、いきいきタスク管理!ワークショップ」。 自分はテキストファイルでの管理が中心。 研究室ではタスク看板的なものも作ってみたんだけど、なかな…

第9回名古屋Scala

7/16 に、第9回名古屋Scala勉強会に参加してきました。 今回は19章と20章。 19章 型のパラメータ化 難しい・・・ 今回はコメント沢山書いたよ! 絵も描いたよ! @rf0444 が人に読める文字を書いている・・・! http://bit.ly/cRJvBy ふぁぼったー / bleis : …