2010-01-01から1ヶ月間の記事一覧

計算機言語で定理証明 第2回

ATNDにページを作っておきました。http://atnd.org/events/2989恐らく今回の問題とかはWikiの方に書く(もしくは参加する人がガンガン書き込んでください)ので、興味の有る方はそちらも見てください。 (ATNDの参考URLにWikiのURLがあります)

限定継続なし版

http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20100124#p01 特に何がやりたい、とかは無かったんですけど限定継続の型がどないや！！っていうのを埋め込んで調べてみたかったのでというのがありました。 それでつまらない事を雑談会の時に話してしまったの…

ぼくもしゅうしょくしないと

金曜日ぐらいから採用試験の問題を考えていたのですが、自分のPCに溜め込んでいてもどうにもならないので折角だから書いてみます。いやそれよりも、MacBookさんの容量が大変です・・・どうしてこうなった。 あとプリンスオブペルシャのPS3版はちょっとうーん…

メモ

POPL2010論文読み会(http://www.cse.psu.edu/popl/10/program.html) [私は気になった∧読めるやつだけ] Verified Compilerな話が多い Verified Just-In-Time Compiler on x86 (http://lambda-the-ultimate.org/node/3768) A Verified Compiler for an Impure …

ぷちます、買いました??

-- "A Tutorial on [Co-]Inductive Types in Coq" -- 3.4 Case Analysis and Logical Paradoxes の Agda2版です。 -- Strictly Positiveが要請される１つの理由 module Paradox where open import Data.String data False : Set0 where data Nat : Set0 wher…

これはもうだめです

{-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiPa…

小さい例(解決)

{-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FunctionalDependencies #-} class Nons nons_a nons_b | nons_a ->…

実装したい(2)

GHCのバージョンは6.10.4です。 {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInst…

継続操作を持つ言語をHaskell上で実装したい(1)

(そもそもEDSLって言うのかなぁ) (DomainにSpecificじゃないですし、なんというか、簡単な言語をHaskell上で表現する、encode、まぁ埋め込むでも良いんですがなんと言えばしっくりくるのか) {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} da…