20110305_14

開催情報

• 日時：3/5 13:00-19:00
• 場所：豆蔵トレーニングルームB
• 参加者数：6名

アジェンダ

• ガリグ先生の今年のレポート課題をみんなで解く
• QCon Tokyo 2011で@kencoba と @yoshihiro503 がAlloy,Coq,SPINのお話をする
• ClojureでSimple Theorem Proverを実装してみた
  • 元は"Programming Language Theory and Its Implementation"という本のCommon Lispの実装。
  • "Handbook of Practical Logic and Automated Reasoning"というOCamlを使う本もあるよ。
• Clojureでオントロジー記述
• 社内でAlloy発表をしてみた
  • 割と食いつきが良かった
  • 「どうしてここだけ手続きなの？」という質問も出た。Alloyの文法だけ見て誤解している。
• F#トレーニングコース「現場で活かす関数型プログラミング(F#編)」3/28やります。
• HOL-OCL
  • IsabelleでOCLを証明する (http://www.brucker.ch/projects/hol-ocl/)
• CoqでRegExpを実装する
  • Yacc is Dead (LtU)
  • カーゴカルト・パーシング
• 形式手法普及セミナー(2/14)参加の感想
  • 図式入力するより、テキスト入力したものが図式表現されるほうがうれしい。
  • シーケンス図をテキスト入力できるツール
  • http://plantuml.sourceforge.net/
    • http://sdedit.sourceforge.net/example/index.html
    • http://blockdiag.appspot.com/seqdiag/
• "Category Theory" Steve Awodey
  • 最初から読んでも訳が分からない。まず後ろから読んで、コンピュータとの繋がりを把握したほうが良い。
  • 次回勉強会では、CoqでMonadをやろう。
  • Concurrent CleanではMonadはダサいってことになってる

コメント、質問