「コンパイルした結果がソースコードと等価である」といった高度な性質まで検証できない／…普通は「定理証明器」といわれますが、すごく強力な型(dependent type)を持ったプログラミング言語とみなすこともできます。

mind のブックマーク 2006/04/18 14:00

<blockquote class="hatena-bookmark-comment"><a class="comment-info" href="https://b.hatena.ne.jp/entry/1772067/comment/mind" data-user-id="mind" data-entry-url="https://b.hatena.ne.jp/entry/s/sumii.hatenablog.com/entry/20060418/1145330147" data-original-href="https://sumii.hatenablog.com/entry/20060418/1145330147" data-entry-favicon="https://cdn-ak2.favicon.st-hatena.com/64?url=https%3A%2F%2Fsumii.hatenablog.com%2Fentry%2F20060418%2F1145330147" data-user-icon="/users/mind/profile.png">関数型言語マニアのための論文紹介６：定理証明器で書かれたCコンパイラ - sumiiのブログ</a><ul class="comment-tag" style="list-style: none; margin: 0px;"><li style="float: left">[<a href="https://b.hatena.ne.jp/q/%E8%A8%98%E5%8F%B7%28image%29">記号(image)</a>]</li><li style="float: left">[<a href="https://b.hatena.ne.jp/q/programming%28%E8%A8%88%E7%94%BB%29">programming(計画)</a>]</li><li style="float: left">[<a href="https://b.hatena.ne.jp/q/%E8%AD%98%E5%8F%B7%28%E8%A8%80%E8%AA%9E%29%E7%B3%BB">識号(言語)系</a>]</li><li style="float: left">[<a href="https://b.hatena.ne.jp/q/4._Equivalent%28%E5%90%8C%E9%A1%9E%29">4._Equivalent(同類)</a>]</li><li style="float: left">[<a href="https://b.hatena.ne.jp/q/%EF%BC%95_%E8%A8%80%E5%8F%8A%28Meta.Escape.Quote%29">５_言及(Meta.Escape.Quote)</a>]</li><li style="float: left">[<a href="https://b.hatena.ne.jp/q/reasoning%28%E5%88%B6%E5%BE%A1%E5%AE%9F%E8%A1%8C%29%7Cdebug">reasoning(制御実行)|debug</a>]</li><li style="float: left">[<a href="https://b.hatena.ne.jp/q/%22_%20function%7C%CE%BB%22">_ function|λ</a>]</li><li style="float: left">[<a href="https://b.hatena.ne.jp/q/.%E8%AB%96%E7%90%86%E7%B3%BB">.論理系</a>]</li></ul><br><p style="clear: left"> 「コンパイルした結果がソースコードと等価である」といった高度な性質まで検証できない ／…普通は「定理証明器」といわれますが、すごく強力な型(dependent type)を持ったプログラミング言語とみなすこともできます。</p><a class="datetime" href="https://b.hatena.ne.jp/mind/20060418#bookmark-1772067"><span class="datetime-body">2006/04/18 14:00</span></a></blockquote><script src="https://b.st-hatena.com/js/comment-widget.js" charset="utf-8" async></script>

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

関数型言語マニアのための論文紹介６：定理証明器で書かれたCコンパイラ - sumiiのブログ

sumii.hatenablog.com2006/04/18

Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. Xavier Leroy. POPL 2006. http://pauillac.inria.fr/~xleroy/publi/compiler-certif.pdf ソースコードとか...

13 人がブックマーク・3 件のコメント

他のコメントを読む

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

はてなブックマーク

関数型言語マニアのための論文紹介６：定理証明器で書かれたCコンパイラ - sumiiのブログ

はてなブックマーク

公式Twitter

はてなのサービス