産総研：システム検証研究センター：CVS研修コース「Agdaによる仕様記述」
研修コース「 Agda による仕様記述」開催のお知らせ ■コース概要 近年、体系的にシステムを開発する手段の一つとして数理的技法(形式手法)が注目を集めています。例えば形式仕様記述の枠組みを使うと、仕様や設計から曖昧さをなくし、全体の整合性を保証することができます。結果として設計書や実装に不具合の種が入り込むことを防ぐことができます。 本コースでは、形式仕様記述の概要とその実際を講義と演習を通して実感して頂きます。演習環境として用いるツール Agda は(１)関数型プログラミング言語(２)形式仕様の処理系(３)定理証明支援系の側面を持つツールです。本コースでは(１)(２)の側面を使い、抽象的なデータの定義と関数を用いてシステムを記述すること、記述を支援する Agda の機能と操作法を扱います。演習の時間を多くとり、実例と経験から形式仕様記述を理解できるコースとなっています。 ■目標 (１
はじめての Coq - zyxwvの日記
Coq などの定理証明系に興味を持っている人は少なくないと思うのですが、やっぱり最初の一歩を踏み出すのは大変。web 上の Coq チュートリアルは、Coq 処理系の機能を説明しているだけで、数学の素養がない人(普通の情報系の学生)が実際に関数の性質を証明するためにどうしたらいいかが書いてあるわけじゃないし。 だって「(a -> b -> c) -> (a -> b) -> a -> c" を証明してみましょう」とか言われても全然やる気にならないじゃん。そんなことを証明するために Coq を使いたいわけじゃない！ そんなわけで、ocaml-nagoya の合宿の機会を利用して id:yoshihiro503 さんと id:suer さんに、Coq をプログラミング言語として使う場合の基本を教えてもらってきました。特に id:yoshihiro503 さんは少なくとも僕から見ると Coq M
OCamlのまなびかた - まぁ、そんなもんでしょう。
いけがみさんが素晴しいエントリをあげてらっしゃいます。Inemuri nezumi diary(2009-05-03)。そこで「OCamlのまなびかた」について思うところを改めて書きます。 まず、Web上のチュートリアルを読めば、ざっくりOCamlがどういう言語なのか分かるかと思います。次の二つがお勧めです。 http://www.ocaml-tutorial.org/jaObjective Caml 入門 一緒にOCamlをインストールして使ってみながら学べば、より効率的です。 $ sudo apt-get install ocaml; sudo apt-get install ocaml-mode lennyのパッケージは3.10系でバージョンが一つ古いので、こだわる人はLatest Objective Caml releaseからソースを取って来てコンパイルして下さい。./confi
Users Meeting - OCaml.jp
縺薙�ｮ繝壹�ｼ繧ｸ縺ｯ譛�蠕後↓譖ｴ譁ｰ縺輔ｌ縺ｦ縺九ｉ1蟷ｴ莉･荳顔ｵ碁℃縺励※縺�縺ｾ縺吶�よュ蝣ｱ縺悟商縺�蜿ｯ閭ｽ諤ｧ縺後≠繧翫∪縺吶�ｮ縺ｧ縲√＃豕ｨ諢上￥縺縺輔＞縲� OCaml Meeting 2009 in Tokyo (蟷ｳ謌仙ｻｿ荳�蟷ｴ譚ｱ驛ｽ螟ｧ鬧ｱ鬧昜ｼ�) 縺薙�ｮ繧､繝吶Φ繝医�ｯ逶帶ｳ√�ｮ縺�縺｡縺ｫ邨ゆｺ�閾ｴ縺励∪縺励◆縲ゅ＃蜿ょ刈鬆ゅ＞縺溽嚀讒倥�√≠繧翫′縺ｨ縺�縺斐＊縺�縺ｾ縺励◆縲� 逋ｺ陦ｨ雉�譁吶ｄ蜍慕判縺檎ｽｮ縺�縺ｦ縺ゅｊ縺ｾ縺吶�ｮ縺ｧ縲√＃蜿ら�ｧ縺上□縺輔＞縲� 髢｢謨ｰ蝙玖ｨ�隱� OCaml縲�1994蟷ｴ縺ｫ螟ｧ蜈�縺ｨ縺ｪ繧� CAML 縺悟ｮ溯｣�縺輔ｌ縺ｦ莉･譚･縲�髟ｷ繧峨￥遐皮ｩｶ閠�逕ｨ縺ｮ縲後♀繧ゅ■繧�縲阪↓逡吶∪縺｣縺ｦ縺�縺� OCaml 縺ｧ縺吶′縲√◎縺ｮ繝励Ο繧ｰ繝ｩ繝縺ｮ螳牙�ｨ諤ｧ繧剃ｿ晁
未来言語Agda - 数学猫の生活と意見
最近Agdaを触る機会があったのだが、Agdaこそ未来のプログラミング言語ではないかという気がしてきた。ここでは行列の転置をする関数を定義することで、Agdaでのプログラミングがどんなものか紹介したい。その前に一言:Agdaは定理証明系として紹介されることが多い。これはAgdaにとって不幸なことだ。確かにAgdaの型システムは強力なので、例のカリーハワード同型により、型を命題、プログラムを証明とみなすことができる。ただし、私の印象ではAgda上は数学の証明をしやすいようにはそんなにはできていない。Agdaで証明するには、ある型をもつ定数なり関数を定義することになるわけだが、定義した関数がその型を持っているかことを型チェッカに説得するために、型チェッカの詳しい挙動について理解していなければならない。むしろ、Agdaは依存型をもつプログラミング言語と思った方がよいと思う。依存型とはなにかは例を
Agda 練習 - zyxwvの日記
あまりわかってないけど、とりあえずいくつか適当な関数を書いたのでメモ。依存型うける(気がする)。 agda2 の emacs モードが使いこなせないのと関数を実行する方法がわからんのが問題である。 module NList where data Nat : Set where zero : Nat succ : Nat -> Nat _+_ : Nat -> Nat -> Nat zero + n = n (succ m) + n = succ (m + n) _*_ : Nat -> Nat -> Nat zero * _ = zero (succ zero) * n = n (succ m) * n = m + (m * n) data List (A : Set) : Nat -> Set where [] : List A zero _::_ : {n : Nat} -> A ->
Lambda Tamer
The Lambda Tamer project tackles the issues surrounding computer formalization of programming languages and their tools, based around the Coq proof assistant. The Lambda Tamer methodology centers on higher-order and dependently-typed abstract syntax and aggressive automation. The main project output is a library of Coq definitions, theorems, and tactics in support of building certified compilers f
Untitled Document
3. Arithmetic omega - Presburger arithmetic (propositional formulas, with equalities, inequalities, for nat and Z) auto with arith - ring - associative commutative rewriting field - equalities in commutative fields (like ring, but with division) fourier - linear inequations with propositional structure, on real numbers 4. Induction Introduction (prove inductive facts) apply - treat each constructo
連載：C# 3.0入門 第1回 ラムダ式 − ＠IT
C# 3.0とは何か？ C#も順調にバージョンアップを重ね、ついに「3.0」である。連載を開始するに当たり、前置きとしてこの連載で扱うC# 3.0とは何かを簡単に紹介しておこう。 C# 3.0は、動的かつタイプセーフなオブジェクト指向プログラミング言語である。「動的」とは、実行するまで内容が確定しない要素が多いことを意味し、「タイプセーフ」とは、あらゆるデータに「型」が存在し、コンパイル時、あるいは実行時にそれが厳格にチェックされることを意味する。そして「オブジェクト指向プログラミング言語」とは、データとプログラムの入れ物である「オブジェクト」を前提とした言語であることを示す。 しかし、これらの特徴はC# 2.0から継承されたものであって、必ずしもC# 3.0固有のものではない。C# 3.0ならではの特徴とは何だろう？ 筆者の個人的な印象だが、C# 3.0は言語が持つ個々の機能について技術
すえひろがりっっっ!(SoftWareメモ)
ruby プロファイル $ ruby -r profile hoge.rb 2008-06-09 02:58 | ruby | sue | comment 0 TeamViewer TeamViewer なにこれ． すげぇ． P2P 的な VNC ? 2008-06-01 16:52 | ツール | sue | comment 0 [Excel]行の自動調整 改行を打たなくてもセルの高さが自動で変わるようにする． ホーム > 配置 > 折り返して全体を表示する 2008-05-22 16:29 | Excel | sue | comment 0 OSのディストリビューションを調べる方法 http://oshiete1.goo.ne.jp/kotaeru.php3?q=2393841 より 1) Debian系 Debian/GNU Linux # cat /etc/deb
関数型言語によるWeb開発 の編集 - ocaml-nagoya
PukiWiki 1.4.6 Copyright © 2001-2005 PukiWiki Developers Team. License is GPL. Based on "PukiWiki" 1.3 by yu-ji. Powered by PHP 4.3.8. Skin by YEAR OF THE CAT
technological blog
[PR]上記の広告は3ヶ月以上新規記事投稿のないブログに表示されています。新しい記事を書く事で広告が消えます。 Ocsigenで再帰するフォームを作ってみた。 OcsigenのチュートリアルのActionというところを真似してみた。 作ってみたページの外観↓ 再帰するフォーム(html)（入力しても意味ないよ） 以下はそのコード open XHTML.M open Eliom open Eliom.Xhtml open Lwt let list_mapi f l = let rec local i = function | [] -> [] | hd::tl -> f i hd :: local (i+1) tl in local 0 l let mylist = ref [] let table_of_hitchart () = table (tr (td[pcdata "[トラック]"
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
関数型プログラミング言語「Agda」の研修コースを産総研が開催 | スラド デベロッパー
Slides for Tsinghua Coq Summer School
ITプランニング OCamlのページ