ATSプログラミング入門
この本は Introduction to Programming in ATS の日本語訳です。 日本語訳の維持管理は JATS-UG - Japan ATS User Group が行なっています。 翻訳に参加するには ATS2公式マニュアルの日本語訳 を参照してください。 プログラミング言語としての ATS は豊かな構文と機能を両立しています。 この本では ATS の中心となる機能を読者に解説します。 それらは基本的な関数型プログラミング、単純な型、(再帰的に定義された) データ型、多相型、依存型、線形型、定理証明、定理証明によるプログラミング (PwTP)、そしてテンプレートを使ったプログラミングなどです。 一般的なプログラミングに馴染みのある読者を仮定してませんが、この本は相当のプログラミング経験のない読者には少し難しいかもしれません。 All rights are reserve
アルゴリズムデザインと定理証明(その1) - golb erutuf
Coq | 21:54この記事は Theorem Proving Advent Calendar 2011 の 22 日目のために書かれた記事です。 Pearls of Functional Algorithm Design というアルゴリズム本の問題を、Coq で解いて証明を付けてみます。ちょっと長くなってしまったので、二回か三回に分けて書きます。はじめに（読み飛ばしてもいいよ）定理証明はタイヘンです。疲れます。Coq や Agda などの定理証明支援系言語は、もうちょっと賢くなってくれれば流行るかもしれませんが今のままだと一部で使われるだけで留まるでしょう。 それなら今 Coq や Agda の勉強なんてしなくて良いのではないか。一部のスゴイ人たちが証明支援系を発達させてくれるのを待ちがら、自分は淡々とテスト、テスト。頑張ってね、スゴイ人たち。… … のっけから何を言い出すんだ。同意す
超未来言語 Gallina - yoshihiro503
LL Future (2008-08-30)今井宜洋 (yoshihiro503) 次 : sm4505381 (shelarcy) 最初: sm4481852 (LL Future 開会宣言) マイリスト: mylist/8224180http://ll.jus.or.jp/2008/
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Haskell で LK の定理証明系を書いた - これは圏です
