TSG Advent Calendar 2015 - Adventarの12/13の記事です。 序文 - pCICとは pCICはPredicative Calculus of (Co)Inductive Constructionsのことで、coqの型システムのことです。 定理証明支援系と言われるcoqですが、そもそもcoqで「証明する」とはどういう…

CPU実験 Advent Calendar 2015 - Adventarの記事です。特別面白そうな話題は思いつかなかったのでこれまでの経緯をまとめただけです。 アーキテクチャについて まずは今回自分が作成したコアについて簡単に説明しておく。 tomasuloのアルゴリズムを使ったア…