# トラックバックをバラまいてしまいました m(_ _)m スミマセン…型レベルプログラミング会議 に行ってきました。 帰りの新幹線でこれを書いています。随時更新予定。 私の発表 最後の TCast がメインなのですがそれはソース参照 スライド1とHaskellソース ht…

sumiiさんの記事によれば，どうも私は [お勉強]とタグをつけたのをいいことにデマを振りまいていたようなので訂正しました．型付きλ計算の型でcharacterizeしてるから論理的，というのなら，正直 Curry-Howard同型による，という説明でもそれほど間違ってな…

Windows Server の話． 背景 ActiveDirectory は LDAP プロトコルで認証できる． LDAPでは， CN=hogehoge,OU=foobar,... という形(DN)で エントリを一意に指定する． 現象 某F社検疫が通らない 原因 Windows の 「ActiveDirectory ユーザとコンピュータ」か…

ATTAPL続き． 論理関係とは 論理関係は λ計算の項の間の2項関係で, 型でインデックスがついている(つまり型を含めれば3項関係). 論理関係は「論理的」な関係である(Curry-Howard的な意味で). すなわち，論理関係とは R(s1, t1, T1->T2) かつ R(s2, t2, T1) …

ATTAPLの6章は 論理関係という方法を使ったプログラムの等価性検査について書いてある．6.3節では, 前準備として, 基本型がプログラムの等価性に影響を与える場合について述べている．ここではλ計算にUnit型を入れてプログラムの等価性を議論している. Unit…