Introducing PeaCoq - COQ EN STOCK
What is PeaCoq? Over the past year, I have developed a Coq frontend called PeaCoq (not to be mistaken with Yves Bertot’s Pcoq). If you wish to play with it before or while reading this article, I made an online version available here. Note that it will reset after 15 minutes of inactivity, and that it might go down any time! There have been several attempts at improving user interfaces for proof a
Support for writing GHC passes in Coq
16-Apr-2011: Now branching from the official ghc base git repo 19-Mar-2011: Things should be working again; I did my own darcs-to-git on the base repo 12-Mar-2011: The “base” repository has moved from darcs to git 10-Mar-2011: The repository names have changed; see below In order to implement heterogeneous metaprogramming for GHC, I have produced a complete formalization of System FC1 in Coq. The
プログラミングCoqの2章をHaskellに翻訳してみた - maoeのブログ
皆さん、小悪魔CoqチュートリアルことプログラミングCoq読んでいますか？僕は大変楽しく読ませていただいています。今日第2章にあたるProof-editing mode であそぼうが公開されました。今回はCoqの証明支援の側面がよくわかる章になっていて興味深いのですが、扱っている命題はまだ簡単で、Haskellでも十分表現できそうです。 というわけでHaskellに翻訳してみました。 今回、Haskellの拡張をいくつか使っています。 Coqの表記と対応関係を取るためにExplicitForAll（Rank2Typesで自動的に有効になる） prop1で、forall付きの型を引数に取る関数の型を表現するためにRank2Types orとandを表す型を演算子で表すためにTypeOperators こうしてみてみると、Coqが自動的に作った仮定がHaskellにおける仮引数に対応づけられて
brainfuck interpreter in Coq - まめめも
Haskell 、Erlang の次のブームは Coq に違いありません。とりあえず基本ということで、Coq でひねりのない brainfuck インタプリタを書いてみました。動作例。Coq のコードが色づけできないとは何事か。 Eval compute in (finite_execute " +++++++++[>++++++++>+++++++++++>+++++<<< -]>.>++.+++++++..+++.>-.------------.<++ ++++++.--------.+++.------.--------.>+. " "" 500). = "Hello, world!"%string : string 残念ながら (?) Coq では停止性が保障された関数しか定義できません。ここでは最大評価ステップを指定しないといけないという仕様にしてごまかしています (引数の 50
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
http://blog.ezyang.com/2014/03/haskell-for-coq-programmers/
Can I extract a Coq proof as a Haskell function?
