プログラミング言語の基礎概念を学んでる - はこべにっき ♨
プログラミング言語の基礎概念 (ライブラリ情報学コア・テキスト) 作者: 五十嵐淳出版社/メーカー: サイエンス社発売日: 2011/07メディア: 単行本購入: 6人 クリック: 60回この商品を含むブログ (12件) を見る この本を読んで学んでる。まだ半分くらいで関数の定義とかについて勉強してる。 プログラミング言語の動作を数学的に厳密に記述する方法を順番に教えてくれるという内容で、記述には導出システムが用いられてる。基本的な算術式からはじまって、変数の定義や関数の定義、パターンマッチや型システムなど、様々な言語の機能を推論規則によって定義する方法を教えてくれる。与えられた規則が意味的に意図したものを表しているかの証明だけでなく、証明のやり方もくわしく説明されていて丁寧でたすかる。 おもしろいのはこの本のためのオンラインの演習システムというのがあって、本の中で与えられた導出システムに
CFML -
以前に、CFMLというものがあるというのを教えてもらった(のは一ヶ月半前)ので、触ってみた。Characteristic Formula generator for MLの略らしい。サイトの下の方に論文リストもあるし、色々なアルゴリズムを証明した例もある http://www.chargueraud.org/softs/cfml/ Coqのようなproof assistantにしろ、Alloyのようなモデル検査器にしろ、人間の考えの正当性を確認するには使えても、実際のコードの正当性の確認とは乖離がある。CoqのExtractというのはあるけど、限りなくバグが少ないとしても遅いコードとかには価値がないケースは多いし、そもそも、どっかの誰かが書いたコードが既にあった時、どうすんのかみたいな話もあるので、色々困る。というわけで、直接コードの検証をしましょうというのが趣旨だと思う なんかCoq-8
なぜCoqが重要か
結論 最強のプログラム検証器 最強の関数型言語 最強のプログラム検証器 Coqは最強の表現力を持つ仕様記述言語を使う 仕様記述言語は検証したいこと を記述するための言語 表現力は検証器によって全然違う 表現できる範囲が、検証器の限界 Coqのそれは高階述語論理 ← 最強 最強のプログラム検証器 Coqを使うためにはPhDが必要? 高校生でも練習すればできる (c.f. プログラミングCoq) 最強のプログラム検証器 証明を人間が与えるのが大変？ タクティックによる自動化はOCamlでいくらでも可能 型チェッカはタクティックと独立なので安全 既にomegaなどの自動証明アルゴリズムを実装したタクティックあり 最強の関数型言語 Coqは(型の表現力が)最強の関数型言語 型の表現力が最強 型推論は完全ではない 停止性は保証しなければならない 注意: ここでの関数型言語とは (ラムダ計算を基礎とし
何度見ても衝撃的な日本のお家芸の論文数カーブ（国大協報告書草案１８） - ある医療系大学長のつぼやき
鈴鹿医療科学大学学長、元国立大学財務・経営センター理事長、元三重大学学長の「つぶやき」と「ぼやき」のblog 今回は、各学術分野別の論文数の推移を、論文絶対数および人口当り論文数で列挙していきます。日本の「強み」「弱み」を知ることが目的だったのですが、前回のブログで、日本はすべての学術分野で弱くなっており、すでに効果的な「選択と集中」ができるような状況にはないことをお話ししましたが、今回の検討でも、同じ感想を持ちました。 特に、日本のお家芸と言われた「物理・化学・物質科学」分野の論文数が、2004年の国立大学法人化を契機に、明確に減少しているカーブは、何度見ても衝撃的です。もう、そんなカーブを見せられても慣れっこになって、何も感じない人もいるかもしれませんが・・・。 そして、韓国、台湾、中国などの新興国が、日本が過去に優位性を保っていた産業競争力を凌駕したことについて、技術の流出や経営戦略
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
