まともな型クラス への入門： 関数型とオブジェクト指向の垣根を越えて - 檜山正幸のキマイラ飼育記 (はてなBlog)
2016年9月に次の記事を書きました。 関数型プログラミングとオブジェクト指向について、何か書く、かも タイトルからして引き続く記事を予告しているのですが、その予告を実行することができませんでした。タイトル中の「何か」とは「型クラス」のことです。上記の記事の最後の部分は： 関数型プログラミングにもオブジェクト指向にも関係があって、今後重要度を増すであろう「型クラス」ですが、今述べた（愚痴った）ような事情で（あと、C++のコンセプトは宙ぶらりんだし）、説明の方針も題材も定まりません。でも、いつか、何か書く、かも。 今回この記事で、予備知識をあまり仮定しないで型クラスの説明をします。言いたいことの1/3くらいは書きました。1/3でも長い記事なので、ぼちぼちと読んでもらえれば、と。書き残したことは最後に触れます。いつか、1年はたたないうちに(苦笑)、続きを書くつもりです。 内容： Haskell
Coqはチューリング完全 -- Ltacでbrainf*ckインタプリタを書いた - Qiita
この記事は、Theorem Prover Advent Calender https://qiita.com/advent-calendar/2017/theorem-prover のために書かれました。 Coqをある程度知っている人向けの小ネタです。 しばしばCoqの紹介において、「Coqでは停止するプログラムしか書けない」「(そのため)Coqはチューリング完全ではない」と言われることがあります。実はこれ、正しいと言えば正しいのですが、間違いと言えば間違いです。 確かに、Coqで再帰関数を定義するためのFixpoint, Program Fixpoint, Functionといったコマンドはどれも停止性を要求します。そのため、Coqから抽出したプログラムは無限ループを起こすことはなく、その意味で安全性が保証されることになります。 では、何が間違いか？ これは「Coqでは停止するプログラム
新刊『定理証明手習い』と『Goならわかるシステムプログラミング』の発売を開始しました！
新刊『定理証明手習い』と『Goならわかるシステムプログラミング』の発売を開始しました！ 2017年10月19日 ご来店ありがとうございます。 開店以来およそ6ヶ月、ここまで『プロフェッショナルSSL/TLS』と『RubyでつくるRuby』の2タイトルで営業していたラムダノートのWebサイトですが、 久しぶりに新刊の発売を開始します。しかも2タイトルの同時発売です！ 1つめの新刊タイトルは『定理証明手習い』です。 証明といっても、証明するのは数学の定理ではなくプログラムの正しさです。 プログラムの正しさというと、まだまだテストによる検証などが真っ先に思い浮かぶかもしれません。しかし、たとえば「定義した関数があらゆる入力に対して破綻せずに動作するか」をユニットテストだけで検証しつくすことはできません。 そこで、数学で公理から推論規則だけで命題の正しさを証明するように、プログラムでも公理からの等
じぇねらるたんシールの注文方法 - Qiita
概要 ADPRINTというサービスを使って誰でもじぇねらるたんの形のシールを作ってもらうことができる。値段は1枚あたり約12円1。 ProofGeneral とは じぇねらるたんは ProofGeneralというツールの公式キャラクターであるが、このツールはCoqなどの対話的証明支援器で証明を対話的に開発するための Emacs プラグインである。 手順 ADPRINTではじぇねらるたんのデータを入校する前に、シールの大きさやタイプを指定して注文を先にする必要がある。 まずADPRINTの注文画面へアクセス: http://www.adprint.jp/OrderMall/Order/TotalOrder.aspx 画像を参考に項目を入力 左上から順に「シール・ステッカー」「一般接着(ラミネートなし)」「横 50mm x 縦 60mm」 裁断は「特殊系」 数量は欲しい枚数を (500枚以上が
CoqからのCプログラム生成 田中 哲 産業技術総合研究所 情報技術研究部門 2017-07-23 Proof Summit 2017
CoqからのCプログラム生成 田中 哲 産業技術総合研究所 情報技術研究部門 2017-07-23 Proof Summit 2017 2/48 元ネタ ● 既発表の話です ● そのうち論文が出ます ● Safe Low-level Code Generation in Coq using Monomorphization and Monadification Akira Tanaka, Reynald Affeldt, Jacques Garrigue IPSJ SIGPRO 114, 2017-06-09, will be appear at IPSJ JIP. ● ここで出てくる plugin は github にあります – https://github.com/akr/monomorphization – https://github.com/akr/monadification
Agda ハンズオン活動報告
こんにちは、@trigottです。この記事では、社内で行っている Agda ハンズオンの紹介をします。 はじめに Agda とは、依存型の使える関数型プログラミング言語、あるいは定理証明支援系です。Coq などとは違いタクティックは使わず証明項を直接記述するスタイルですが、Emacs 上で対話的に証明を進めるためのインタフェースが用意されているため、効率的に証明を進めることができます。Agda で n * 2 と n + n が等しいことを証明する動画を撮影してみました。雰囲気がつかめれば幸いです。 KLab では月に１回 ALM(All Layers Meeting)という社内勉強会を開催しています。学生のころから Agda が好きで触っていたこともあって、Agda に関する発表をしたところ、先輩からハンズオンを開いてほしいということを言われました。ハンズオンとかやったことないし、Agd
Isabelleについて： 証明支援系は何を目指し、どこへ向かうのか - 檜山正幸のキマイラ飼育記 (はてなBlog)
昨日の記事「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」では、Isabelleのユーザーインターフェースが備えている特徴的な機能である「継続的チェッキング」だけを取り上げました。ここで改めて、証明支援系としてのIsabelleシステムを紹介しましょう。客観的な紹介ではなくて、僕の雑駁な印象記です。 内容： Isabelleの独自な世界 Isabelleの未来 Isabelleの独自な世界 「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」より： PIDE構想は、Isabelleプロジェクト／コミュニティを世の趨勢とは離れた孤立化へと導くのか、それとも、時代がPIDEの先進性にいずれ追いつき、PIDEがスタンダードな証明支援系UIとなるのか？ なかなかに興味深いですな。 Isabelleが世の趨勢と離れるのか？
Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった - 檜山正幸のキマイラ飼育記 (はてなBlog)
以前、証明支援系Coqの記事を書いたことがあります。今日話題にしたいIsabelle（イザベル）は、Coqのライバルと目される証明支援系です。最初のリリースが1986年ですから、実に30年間に渡って開発が続けられています（Coqもほぼ同時期にスタートしています）。十分に枯れた処理系でありながら、現在でも開発は活発で、新しい地平に向けて果敢な挑戦も試みられています。特に、ユーザーインターフェースの改善に熱心で、現在のGUIフロントエンドであるIsabelle/jEditには、驚くべき機能（の卵）が実装されています。 内容： 継続的チェッキング ウェンツェルのPIDE構想 継続的チェッキング 理屈や背景は後回しにして、「継続的チェッキング」を簡単な実例で紹介します。 Isabelleは証明支援系ですが、プログラミング言語Standard ML（以下、SMLと略記）のコードエディタとしても使えま
『ソフトウェアの基礎』のePub版を公開しました。 - みずぴー日記
「Software Foundations(和訳: ソフトウェアの基礎)」はBenjamin Pierce氏らによって書かれたドキュメントであり、Coqによりプログラミングやプログラミング言語の理論が解説されています。基本的な部分から丁寧に解説されているため、Coqの入門書としてもプログラミング言語理論の入門書としても、非常に優れた内容となっています。 今回は、その「ソフトウェアの基礎」のePub版を公開しました。 対応したリーダを用いることで、iPhoneやiPad、Androidで本ドキュメントを読むことができます。 ダウンロード http://proofcafe.org/sf-beta/ からダウンロードできます。 またmobi版もありますが、Kindleを持ってないので、動作確認はしていません。 バグ報告 http://github.com/sfja/sfja へのissues登録
Krakatoa and Jessieを用いた、Javaプログラムの正当性＆安全性証明(アルゴリズムもあるよ！) - 簡潔なQ
概要 Javaプログラムに専用の記法で満たすべき条件を形式的に記述し、それをCoqの問題に変換して手動で証明する。 この記事はCompetitive Programming Advent Calendar 2011およびTheorem Proving Advent Calendar 2011の12日目の担当記事である。 用意するもの Why 2.30 および Why3 0.71 (両方必要) Why 2.30に同梱されているKrakatoa and Jessieを用いる。 Coq 上記ソフトウェアが動作するOS (ここではUbuntu 11.10) なお、Ubuntu上での準備方法は、直前の記事を参照。 流れ Javaコードに、KML(JMLをベースにした仕様記述言語)で仕様を付記する。 Krakatoaを使って、JavaコードをJessieコードに変換。(ちなみに、Cコード+ACSLをJ
Halobet 🎀 Situs Slot Online Terpercaya Gacor 2024
Decrease quantity for Halobet 🎀 Situs Slot Online Terpercaya Gacor 2024 Increase quantity for Halobet 🎀 Situs Slot Online Terpercaya Gacor 2024 Fasilitas Lengkap untuk Pemain Baru Bagi para pemain baru, Halobet menyediakan fasilitas lengkap untuk memastikan Anda merasa nyaman dan terhibur selama bermain di situs kami. Dari berbagai pilihan permainan slot hingga layanan pelanggan yang responsif,
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Using Coq in Docker: The Basics
Loading...
GitHub - krtx/agda-handson: agda handson
証明プログラミング超入門
長文日記
並列代入に対する代入補題の自動証明