TSG Advent Calendar 2015 - Adventarの12/13の記事です。 序文 - pCICとは pCICはPredicative Calculus of (Co)Inductive Constructionsのことで、coqの型システムのことです。 定理証明支援系と言われるcoqですが、そもそもcoqで「証明する」とはどういう…
CPU実験 Advent Calendar 2015 - Adventarの記事です。特別面白そうな話題は思いつかなかったのでこれまでの経緯をまとめただけです。 アーキテクチャについて まずは今回自分が作成したコアについて簡単に説明しておく。 tomasuloのアルゴリズムを使ったア…
大学の冬休みの課題(ハードウェア構成法講義 - 平木研究室)で25bitの小数P()の平方根A(25bit)を求める回路を書くという課題が出たのでその方法を考えた。気の向くうちにと勢いで書いた記事なので分かりにくかったり間違えてたりするかも。 問題の設定 小数の…
PAMについて調べたことのまとめ。内容については十分確認してないのでもしかしたら見当違いな事を書いてるかもしれない。 PAMとは Pluggable Authentication Module 認証処理を行うモジュール群とそれを利用するためのAPIからなるユーザー認証システム http:…
Ubuntuにvimをインストールした時に一緒に入っていたnetrw v147ではディレクトリ名が日本語を含むとき、ディレクトリの移動ができなかったり、ファイルがちゃんと開けなかったりしたので解決法を調べてみた。最初に見つけたのは netrwで全角ではじまるディレ…
Villager Bを解いたのでその記録 大まかな方針だけ書くようにしますが自力で解きたい人は見ないでください 問題の確認 To be more secure I enabled several security options as follows: Randomized addresses of the program (-pie) Protected the stack …
今まで何となく使っていたcoqのタクティックの動作を少し詳しく見てみることにした。ソースコードを読むべきかもしれないけど、まずは実際どう動くかを観察して解釈することにした 以下はその記録 destruct and(/\)のdestruct Goal forall P Q: Prop, P/\Q -…
levelfour君の記事を読んで物理演算エンジンに興味を持ったのでBulletを学んでみることにした。 OSはUbuntu 13.04 Bulletのインストール https://code.google.com/p/bullet/downloads/listからbullet-2.82-r2704.tgzをダウンロードして展開し、そのディレク…
期末試験での現実逃避のため最近改めてCoqに触ってみた。ここでは、その内容と自分の理解について簡単にまとめて書き残すが、不正確な内容が含まれているかもしれない。 関数の連続性、数列の収束 微積分の証明をCoqで扱ってみたいなと思ったので、関係しそ…
mod_rewriteとCGIが使えるけどSSIが(たぶん)使えないサーバーで作業しててふと思いついた こんなのやりたがる人いるかは怪しいし、くだらないかなと思いつつも書いておくやったことは単純.htaccessに、名前が.shtmlで終わるファイルへのアクセスがあった時に…
Twitterでオバマ大統領(@BarackObama)があかり大好きbot(@akari_daisuki)をフォローしているとかいう画像を目にした 少し前からRubyのTwitter Gemを使ってみたかったので、Twitter Gemで検証してみた 環境 まず環境 今回はWindowsでやってみた >ruby -v ruby…