[過去ﾛｸﾞ] Lisp Scheme Part40 [転載禁止]©2ch.net (1002ﾚｽ)
上下前次1-新
抽出解除 必死ﾁｪｯｶｰ(本家) (べ) 自ID ﾚｽ栞 あぼーん
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
ﾘﾛｰﾄﾞ規制です｡10分ほどで解除するので､他のﾌﾞﾗｳｻﾞへ避難してください｡
920: 2018/05/13(日)10:00 ID:V4PsQf4P(1/2) AAS
David Thrane Christiansen のやっている Idris や Pie language といえば、
依存型 (dependent type) を使用した Type-Driven Development かな。
定理証明系の次の話題としては順当なところ。
922: 2018/05/13(日)13:45 ID:V4PsQf4P(2/2) AAS
依存型についてのテキストはこれまでにこういうのが出てるよ。
Edwin Brady "Type-Driven Development with Idris"
Adam Chlipala "Certified Programming with Dependent Types"
Aaron Stump "Verified Functional Programming in Agda"
Edwin Brady と David Thrane Christiansen は協力して Idris を作ったひとで、
今回、Christiansen が Racket 上で Pie language を実装したみたい。
Pie languageの実装を理解させる本が出ることで Type-Driven Development の
低レベルでの詳細が明快になると期待できる感じかな。
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.042s