OCamlで正規表現を微分する - fetburner.core
僕の所属する研究室では毎年Software Foundationsの輪講をやっているんですが，Brzozowski derivativeに基づいて正規表現エンジンを実装し，あまつさえCoqで検証してしまおうといった練習問題が追加されていて大変興味深かったです． 折角practicalなプログラムを書いたのにCoqの中に閉じ込めておくのも勿体ないですし， OCamlで同様の正規表現エンジンを実装し，実行速度を見てみようと思います． *1 2018/12/16 Brzozowski derivativeの定義に誤りがあったため修正 Brzozowski derivativeとは？ ある正規表現が受理する言語の先頭から，文字を取り除いて得られる言語 *2を受理する正規表現をBrzozowski derivativeといい，以下のようにsystematicに求められます． ある正規表現が空文字列を
Coqで学ぶ証明プログラミング！ テストだけでなく「証明」で安全性を保証する - エンジニアHub｜Webエンジニアのキャリアを考える！
Coqで学ぶ証明プログラミング！ テストだけでなく「証明」で安全性を保証する プログラミング言語「Coq」では、プログラムを「証明」して間違いを防ぐことができます。プログラムの正しさを保証できる一歩進んだエンジニアになりましょう！ coqtokyoを主催する今井宜洋さんの解説です。 みなさん、Coqってご存知ですか？ プログラムを証明して間違いを防ぐという優れものです。今回はそのCoqについて、coqtokyoという勉強会を主催している今井宜洋がお届けします。 プログラムをただ作るだけではなく、その正しさを保証できる一歩進んだエンジニアになってみましょう！ Coqって何？ プログラムを「証明する」ってどういうこと？ Coqを使ってみよう Coqのインストール方法 CoqIDE：Coqによる証明開発のフロントエンド Coqで関数プログラミング プログラムの仕様を記述しよう 証明開発モード ゴ
もっと二分探索に証明を付ける - fetburner.core
以前二分探索の正当性をCoqで証明しましたが，この証明スクリプトからOCamlのコードを抽出して実際に競プロに用いようとすると，添字の動く範囲が保証されていないので添字エラーを起こすこともしばしばでした． そこで，依存型を活用して添字の動く範囲も保証しようと思います． 以前の実装 以前Coqで書いた二分探索は以下のように，まずプログラムを書いてから Variable P : nat -> Prop. Hypothesis P_dec : forall n, { P n } + { ~P n }. Function lower_bound_aux offset n { wf lt n } := match n with | O => offset | _ => let m := Nat.div2 n in if P_dec (offset + m) then lower_bound_aux
迷路の試験問題を解いてみた - にわとり小屋でのプログラミング
参考：人材獲得作戦・４ 試験問題ほか: 人生を書き換える者すらいた。 Lv4に評価されるためには、最短性の完全なチェックが必要だったのでCoqで証明してみた。 まず、accessiblesという関数を定義し、以下の性質を証明した。 ここでplengthはパスの長さを計る関数で、Path x pはpがxを起点としたパスであるという述語。endofはパスの終点を求める関数。 Fixpoint accessibles (start : node) (len : nat) : list path := match len with | O => (PUnit start) :: nil | S n' => div_equiv path_equiv_dec @@ (flat_map expand @@ accessibles start n') end. この関数はstartから始まってlenの長さ
にわとり小屋でのプログラミング日記
この記事はTppMark11の問題をCoqでやってみたという内容である。 問題はこちら: docs.google.com 命題論理式と同値であることの定義 命題論理式の定義 Inductive Term := | Var(v : Var.T) | Neg(t : Term) | And(t1: Term)(t2: Term) | Or(t1: Term)(t2: Term) | Impl(t1: Term)(t2: Term) | TRUE | FALSE . 同値であることの定義 変数環境を表すctxを Var.T -> bool の関数で表現し、命題論理式のevalを次で定義した。 Fixpoint eval ctx t : bool := match t with | Var v => ctx v | Neg t => negb (eval ctx t) | And t1 t2 =>
[WIP] Generate Coq files with `make lem-coq` by pirapira · Pull Request #131 · pirapira/eth-isabelle
brainfuck interpreter in Coq - まめめも
Haskell 、Erlang の次のブームは Coq に違いありません。とりあえず基本ということで、Coq でひねりのない brainfuck インタプリタを書いてみました。動作例。Coq のコードが色づけできないとは何事か。 Eval compute in (finite_execute " +++++++++[>++++++++>+++++++++++>+++++<<< -]>.>++.+++++++..+++.>-.------------.<++ ++++++.--------.+++.------.--------.>+. " "" 500). = "Hello, world!"%string : string 残念ながら (?) Coq では停止性が保障された関数しか定義できません。ここでは最大評価ステップを指定しないといけないという仕様にしてごまかしています (引数の 50
Mathematical Components (the book)
About Mathematical Components is the name of a library of formalized mathematics for the Coq proof assistants. It covers a variety of topics, from the theory of basic data structures (e.g., numbers, lists, finite sets) to more advanced results in various flavors of algebra. This library constitutes the infrastructure for the machine checked proofs of the Four Color Theorem and of the Odd Order The
ML勉強会まとめ - type t (* void *)
僕がML情報が集まる会が欲しくて開催しました。 @blackenedgold さん、@khibino さんにご協力頂きましてありがとうございました。 connpass.com 発表一覧 ATSで捕捉されたリアルタイムOSのシステム状態(masterq さん） Real-time OS system state captured by ATS language from Kiwamu Okabe www.slideshare.net リアルタイムOSのChibiOSの紹介とATS2の宣伝（？） ChibiOSは内部的に状態を持っており、API関数を呼ぶときに普遍条件があるけども、 C言語から呼び出すとそれをキャプチャできないのでプログラムが危険になっていました。 それをATS2の依存型を用いて現在のOSのステートを型にエンコードして解決している話でした。 ステートを埋め込むだけならば幽霊型を
2006-09-30
なんとなく。 ;Gaucheで >(define-syntax lambda->match (syntax-rules (lambda) ( (_ ((lambda vars body) arg1 ...)) (match (quote (arg1 ...)) (vars body)) ))) >(lambda->match ((lambda (x y) (+ x y)) 2 3)) 5 >(lambda->match ((lambda (x . xs) (cons x xs)) 2 3 4)) (2 3 4)matchはlambdaより強力です Gaucheで、ファイルユーティリティはfile.utilなのに、マッチングユーティリティはutil.matchなのは、何故なんだぜ？毎回間違える･･･ここらへんの再発明な ;gaucheで (use util.match) (define (c
2013年度前期・数理解析・計算機数学 II
[ ホーム | 講義 ] 2013年度前期・数理解析・計算機数学 II (同 概論II) レポート課題 レポート課題 提出期限 2013年8月2日(金) 講義予定 シラバス 第1回 4月12日 Coq で関数型プログラミング 講義メモ 資料 EmacsでCoqを使う 設定ファイル coq.emacs (.emacs にコピーす る) 第2回 4月19日 Coqの論理 講義メモ 第3回 4月26日 述語論理と帰納法 講義メモ 第4回 5月10日 帰納的な定義と多相性 講義メモ 第5回 5月17日 プログラムの証明1 講義メモ 第6回 5月24日 プログラムの証明1 5月25日 14時半〜17時半 多元307号室 (ご興味の方) Proof Cafe: 先輩達によるCoqの勉強会 第7回 5月31日 プログラムの証明2 講義メモ 6月7日 名大際のため休講 第8回 6月14日 数学的な証明 講
IIJ Research Laboratory
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Verified Functional Algorithms
書くネタがCoqしかない
Coqでbrainfuck処理系書いた - うさぎ小屋
https://github.com/suharahiromichi/doc/blob/master/coq_gitcrc.md
ソフトウェアの基礎(beta) — ソフトウェアの基礎 1.0.2 documentation
m-a-o
Log in to SlideShare
ソフトウェアの基礎