まず主催者だったんだなぁ的な・・・。主催者っていうか・・・。 はじめに皆さん集合時間にルーズで、でもまぁそれを見越しての11:00だったので、最初に来た人は幻のゾンビFLTVが見られました。 見ても何も良い事は無いですけれども。 真っ黒Scheme Schemeの…

発表View more documents from ranha.今回の私の発表は、思考の道具としてのプログラミングという観点から見てのプログラミング言語が未来に向かって持つべき何かを探るというような事でした。あの発表からそんな事が考えられていたという事は、分かる筈もな…

発表者のタイトルや資料 Ustream ヤドカリさん 「真っ黒Scheme」 http://d.hatena.ne.jp/yad-EL/20090830/p1 http://www.ustream.tv/recorded/2072252 natsutanさん 「未来のハードウェア言語」 http://natu.txt-nifty.com/natsutan/2009/08/fltv-0901.html …

http://www.iis.sinica.edu.tw/~scm/2007/agda-exercise-length-indexed-mergesort/ via http://twitter.com/ikegami__/status/3573974552いけがみさんの一言でクイックソートはどうでも良いっていうか、この周辺に4日ぐらい居た気がして、その間他の事があ…

まぁぼくはどこにもフィードバックしてないので、ユーザとして認識されてないんですけど、こういうのは凄く頭のいい、普通の人100人分ぐらいの人達が使ってるので多分大丈夫のはず module TCheckTest where data Nat : Set0 where zero : Nat succ : Nat -> …

割と良く分からないなーって感じになって、ググるとさかいさんの記事が出て来たので、依存和使っててすごいというか、なんで依存和使ってるか分からん感じだったんですけれども、実際やってみると少し分かりました。http://www.tom.sfc.keio.ac.jp/~sakai/d/…

module Proof1 where data List (A : Set0) : Set0 where [] : List A _::_ : A -> List A -> List A rec1 : {X : Set0} -> List X -> List X rec1 [] = [] rec1 (x :: xs) = rec1 [] -- ここのrec1でrec1の停止性を証明出来ないらしい。うーん・・・。 rec1…

filter : {X : Set0} -> (X -> Bool) -> List X -> List X filter p [] = [] filter p (x :: xs) with p x ... | true = filter p xs -- x :: (filter p xs) ... | false = filter p xsfilterをこう書き直して、つまり、[]しか返さないんですけれども、これ…

でません・・・。 natEq : Nat -> Nat -> Bool natEq zero zero = true natEq zero (succ b) = false natEq (succ a) zero = false natEq (succ a) (succ b) = natEq a b boolEq : Bool -> Bool -> Bool boolEq true true = true boolEq false false = true …

natRight : {a : Nat} {b : Nat} -> a NatPair b -> Nat natRight (a natPair b) = b getNatRight : {a : Nat} {b : Nat} -> a NatPair b -> Val b getNatRight (a natPair b) = val b valNat : (a : Nat) -> Val a valNat a = val a body : (length (filter…

けれども、分かりません・・・。 module QSort where open import Data.List open import Data.Bool open import Data.Product data Nat : Set0 where zero : Nat succ : Nat -> Nat Length : {A : Set0} -> List A -> Nat Length [] = zero Length (x &#875…

です

Agdaにはさん付けが良いのか、くんづけが良いのか、その他(って言っても)が良いのか分かりません。あとAgdaは定理証明系の属という呼び方が普通で、それはPrologが人工知能向けだとかっていう(まぁLispが人工知能界隈向きというよりはマシな気がするんですけ…

「もぉ↘にゃどぉぅ↺」じゃないのかむしろ！！？？！

「もぉ↘にゃどぅぉ↺」って感じなんじゃないかなー

亜美真美が言う「もにゃどー」を想像したら、頑張ろう！！って気持ちになった。ドガー。

環境はMacBook 10.5.8でAgda-2.2.4を以下の内容を元にインストールhttp://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.MacOSX最初からHaskell周りのあれこれは入れてたので、2.install from the darcs repository, for the latest sourceの方に基づいて…

暇なのと、FLTVのネタ蒐集を兼ねてJSSST読んでました。http://www.jstage.jst.go.jp/browse/jssst/25/3/_contents/-char/ja/ここの 「モデル生成型定理証明と要素技術」と「論理・制約プログラミングと並行計算」。あと気になったのは(つまり読んでない)のは…

を行ったので、本棚をログとして上げてみました。かわいー本が欲しいです。かわいー本というわけでは無い感じですが、一番下にちっこく映ってる「敷居の住人」は面白いです。

圏合宿が終わった時間が22:00だとかで、やっぱりこれはつくば帰れないよなーって事で、秋葉原のネットカフェへ。実は参宮橋駅前のサークルKサンクスでアイマスねんぷちが買えるというハッピーな出来事がありました。 kawaii!!(圏合宿の時に話に上がった本を…

http://d.hatena.ne.jp/hiroki_f/20090813/1250129085に参加してきました。テキストは層・圏・トポス(竹内外史著)で、米田の補題手前まで。相変わらず数学の本ていうのは「書いている事をそのまま理解する」事が大事だよなーというのを感じたり。 あとは、圧…

FLTVはこれ( http://atnd.org/events/1102 )です。こんかいは画像無しです。でも天海春香さんが登場しています。Finger Tree Translate for RanhaView more documents from ranha.(reverse "amamiharukasan"を順にEmptyに足して行く、ですね。間違ってます。…

今日 8/5 はIDOLM@STER MASTER SPECIALシリーズの最後となるMASTER SPECIAL 06が発売されるので、まずそれを買います。そして次に、ぼくのはじめてのりすぷ！！ どこから処理系を取るんや http://yices.csl.sri.com/http://yices.csl.sri.com/download.shtml…