タグ

coqと情報科学に関するr-westのブックマーク (2)

  • えぷりくす

    http://portal.acm.org/citation.cfm?id=1040305.1040313 今年のPOPLにこんなのがあったそうで、まさしく今 quantitative な analysis をテーマにしてる身としてはちょっと読んでみようかなと思ったり。 それはそうとすみいさんもほそやさんも POPL 通ってて自分はさっぱりうだつがあがらんなあとちょっとがっくり http://www.excite.co.jp/News/odd/00081108087433.html ジョーンズさんの友人の手元に渡るまでの経緯が激しく気になる http://www.nikkansports.com/ns/general/f-so-tp0-050111-0019.html 「鈴木亜美で子3人殺害」に見えた。 処方されたリタリンを試してみた。さすが「合法覚醒剤」の別名を持つだけあって、他の薬が

    えぷりくす
    r-west
    r-west 2007/08/09
    Coqの学習と利用
  • にわとり小屋でのプログラミング

    この記事はTppMark11の問題をCoqでやってみたという内容である。 問題はこちら: docs.google.com 命題論理式と同値であることの定義 命題論理式の定義 Inductive Term := | Var(v : Var.T) | Neg(t : Term) | And(t1: Term)(t2: Term) | Or(t1: Term)(t2: Term) | Impl(t1: Term)(t2: Term) | TRUE | FALSE . 同値であることの定義 変数環境を表すctxを Var.T -> bool の関数で表現し、命題論理式のevalを次で定義した。 Fixpoint eval ctx t : bool := match t with | Var v => ctx v | Neg t => negb (eval ctx t) | And t1 t2 =>

    にわとり小屋でのプログラミング
  • 1