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

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

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