関数型言語haXe

haXe

最近、ocaml-nagoya勉強会でhaXeコンパイラのソースコードを読んでいるので、haXeのプログラムを書きたくなってきた。ということで、ここにいろいろ書いてみます。いろいろ指摘いただけると助かります。http://ocaml-nagoya.g.hatena.ne.jp/yoshihiro503/

2008-10-28

定理証明器Isabelleで計算可能性の証明

Isabell 計算可能性計算複雑性

偶然見つけました。 http://www2.score.cs.tsukuba.ac.jp/4eba3005-1/student/takuya-fujiwara-1/cs30bb30df30ca30fc767a88688cc76599-1/CSseminor2008_Fujiwara_Slides.pdf将来、定理証明器で言語の開発をするようになるのかもしれない。チューリング完全性…

2008-09-15

CoqでPrim言語のサブセットのパーサを実装した。

CSNagoyaのコンパイラを作ろう部門での教科書「コンパイラ入門 C#で学ぶ理論と実践(冨沢高明)」が自宅に届いたので、8章までの部分を復習するために実装してみた。この本ではC#という言語で実装することを念頭に置かれていたが、Coqが好きなのでCoqで実装…

2008-09-06

Lambda Cを実装してみた。

404 Not FoundやはてなダイアリーでλCが話題になっていたので、Lambda C インタプリタを実装してみた。多相型も依存型もサポート。定理証明もできる。Lambda C Interpreterサンプルコード: λ(A:*). λx:A. x （恒等関数） λ(A:*). λ(x:A). λ(y:A). Π(P:Π(a:A)…

2008-09-01

Leightweight Language Future (LLFuture) と、等価変換セミナーに行ってきた。

LL Future LL Futureでは、id:sumiiさんがラムダ式や、ユークリッドのアルゴリズムなどの歴史を語っていたのがおもしろかった。数学でのおもしろい概念は何百年後も利用されるのか。じゃあ今、数学(や計算機科学)でホットな話題が100年後利用されるのかな？…

2008-08-29

LLFutureというイベントに行ってきます。

Gallinaについて軽く話します。

2008-07-14

Coqで依存型

Coq Agda

最近Agdaがはやっているみたいなので、Coqでも依存型（dependent type）を使ってみた。実装したのは長さ n のベクトル型だ。このベクトル型を使うと、空でないとか、長さが等しいとかを型の段階で保証できるので、より安全なプログラムを書くことができるの…

2008-07-02

CoqのソースコードをカッコイイHTMLページにする方法(coqdocを使う)

Coqでプログラムや証明を書いたら、そのソースコードを人に見せたりしたくなるときがある。そのときに便利なcoqdocという機能がある。coqdocはcoqtopやcoqcなどと一緒のところにある。使いかたは以下。 $ coqdoc [Coqファイル.v] ここで、(** コメント *)…

2008-06-23

CoqでProject Euler (problem 44)

Problem44が解けた? - みずぴー日記に触発されて、Project EulerのProblem 44に挑戦してみた。問題44: 五角数は Pk = k(3k-1)/2で生成される. 五角数のペア PmとPnについて, 差と和が五角数になるものを考える. 差を D = |Pm - Pn| と書く. 差 D の最小値を…