例のPHOAS表現の言語の証明可能コンパイラのテキスト//PHOAS表現によって、unfold;simpl;fold中心で証明する

coq
proof

bellbind のブックマーク 2008/11/04 15:27

<blockquote class="hatena-bookmark-comment"><a class="comment-info" href="https://b.hatena.ne.jp/entry/10682553/comment/bellbind" data-user-id="bellbind" data-entry-url="https://b.hatena.ne.jp/entry/adam.chlipala.net/cpdt/" data-original-href="http://adam.chlipala.net/cpdt/" data-entry-favicon="https://cdn-ak2.favicon.st-hatena.com/64?url=http%3A%2F%2Fadam.chlipala.net%2Fcpdt%2F" data-user-icon="/users/bellbind/profile.png">Certified Programming with Dependent Types</a><ul class="comment-tag" style="list-style: none; margin: 0px;"><li style="float: left">[<a href="https://b.hatena.ne.jp/q/coq">coq</a>]</li><li style="float: left">[<a href="https://b.hatena.ne.jp/q/proof">proof</a>]</li></ul><br><p style="clear: left">例のPHOAS表現の言語の証明可能コンパイラのテキスト//PHOAS表現によって、unfold;simpl;fold中心で証明する</p><a class="datetime" href="https://b.hatena.ne.jp/bellbind/20081104#bookmark-10682553"><span class="datetime-body">2008/11/04 15:27</span></a></blockquote><script src="https://b.st-hatena.com/js/comment-widget.js" charset="utf-8" async></script>

このブックマークにはスターがありません。
最初のスターをつけてみよう！

Certified Programming with Dependent Types

adam.chlipala.net2008/11/04

This is the web site for a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof ...

42 人がブックマーク・6 件のコメント

他のコメントを読む

＼コメントがサクサク読めるアプリです／

はてなブックマーク

Certified Programming with Dependent Types

はてなブックマーク

公式Twitter

はてなのサービス