タグ

functional-programmingとspecificationに関するnabinnoのブックマーク (2)

  • 2012年に形式手法を学び始めるならこの7冊 - masateruk’s blog

    前エントリー「僕が形式手法を学び始めたときに読んだ10冊 - masaterukの日記」のラインナップはあまりに入手困難なものばかりだったので、2012年に始めるならということで改めて選んでみた。 1冊目。 VDM++によるオブジェクト指向システムの高品質設計と検証 (IT architects’ archive) 作者: ジョン・フィッツジェラルド、ピーター・ゴルム・ラーセン、ポール・マッカージー、ニコ・プラット、マーセル・バーホフ,酒匂寛出版社/メーカー: 翔泳社発売日: 2010/08/03メディア: 大型購入: 1人 クリック: 32回この商品を含むブログ (8件) を見るVDM++の。形式手法を学び始めるならこのから始めると取っ付きやすいのではないかと思う。高級言語をつかった陽関数定義(実行可能形式)でモデルをがんがん書いて、シミュレーションとテストでモデルを洗練していくや

    2012年に形式手法を学び始めるならこの7冊 - masateruk’s blog
  • 型付きラムダ計算 - Wikipedia

    型付きラムダ計算(かたつきラムダけいさん、英: typed lambda calculus)とは、無名の関数の抽象表現にラムダ () というシンボルを用いる型付き形式手法である。型付きラムダ計算は基礎的なプログラミング言語でもあり、MLやHaskellなどの型付き関数型言語の基盤であり、さらには型付き命令型プログラミング言語の間接的な基盤とも言える。また、カリー・ハワード同型対応によって数理論理学と証明論とも密接に関連しており、圏論のクラスの内部言語と見なすこともできる。例えば単純な型付きラムダ計算はデカルト閉圏 (CCC) の言語である。 ある観点から見れば、型付きラムダ計算は型を持たないラムダ計算を改良したものと言えるが、別の観点からは、より根的な理論と見ることもでき、型を持たないラムダ計算の方が型が1つしかない特殊ケースと見ることができる。 様々な型付きラムダ計算がこれまで研究され

  • 1