http://ranha.kerox.info/nandemo/?Comparative+StudyなぜかWikiを建てたので、埋まってない所を勝手に埋めたり、分からない所はとことんコメントを書いたりしてください。 OCamlの所が完全に人間足りてない感じです。あとC#

前編 4/24土曜は、Olegさんの話を聞く会を聞く為に東京に来ました。 朝方までPS2でパチンコのようなものをやった挙げ句、全然大学で眠れなかったとかいうのもあって、ただでさえ辛い早起きがウルトラ辛かったような気がします。取りあえず最初の話は、Abstra…

Signature File sig lc. kind tm,ty type. type c tm. type app tm -> tm -> tm. type abs (tm -> tm) -> tm. type top ty. type arrow ty -> ty -> ty. type ty ty -> o. type of tm -> ty -> o. type step tm -> tm -> o.Module File module lc. ty top. t…

tm : type. step : tm -> tm -> type. sn : tm -> type. sn_ : ({U:tm} step T U -> sn U) -> sn T. lem : (sn T) -> (step T U) -> (sn U) -> type. %mode lem +D1 +D2 -D3. lem_pr : lem (sn_ Pred : sn T) (StepTU : step T U) (Pred U StepTU). %termina…

http://atnd.org/events/4060 要旨 去年に引き続いての開催。 どういう人が、どういう内容物であの入試をくぐり抜けて来たのかというのを肌で感じよう、というのが目的です。 特に ●大学に入学して/入学するまでに何をしたか、をスライドにし他人に発表して…

{- 1個の時 _1 a1 a2 a3 = a1 (a2 a3) -} {- 2個の時 Prelude> :t (.)(.) (.)(.) :: (a1 -> b -> c) -> a1 -> (a -> b) -> a -> c (.) a1 a2 a3 = a1 (a2 a3) (.)(.) a2 a3 = (.) (a2 a3) = (\a4 a5 -> (a2 a3) (a4 a5)) _2 a1 a2 a3 a4 = (a1 a2) (a3 a4) P…