2014-08-14 貧乏帰省の顛末 現在東北の大学に通っているんですが、実家から遠くに住んでいると帰省の交通費が馬鹿になりません。*1そこで、何とかして安く帰ろうとしたのですが一悶着あったという話。 *1:仙台高松間を新幹線で往復すると5万円程度にもなる 続きを読む
2013-12-21 モータドライバの設計 電子回路 動機 昔、モータードライバを自作しようと試みた事がありました。しかし、自作のドライバはロボコンで用いられていた既製品に対して信頼性で劣っており、既製品の出力に不満が無かったために置き換えられませんでした。 続きを読む
2013-09-22 簡単な式の評価器を証明駆動開発 プログラミング言語の基礎概念 Coq OCaml EvalML1Errにおける評価の全域性の証明でML1*1のすべての式に評価される値が存在することが分かったので、式を評価する関数書いてみたいと思います。また、せっかくCoqで書いたので関数が妥当であるかの証明とOCamlソースコードの出力も行おうと思います。 *1:プログラミング言語の基礎概念に登場する、MLのサブセットのような言語 続きを読む
2013-09-19 EvalML2における評価の一意性の証明 プログラミング言語の基礎概念 Coq 前回、前々回は四則演算程度しか持たない導出システムについての証明でしたが、今回は変数束縛や環境を持つ導出システム、EvalML2における評価の一意性を証明しようと思います。例によって元ネタはプログラミング言語の基礎概念です。 続きを読む
2013-09-07 FreeBSDにAjhcをインストールするときに躓いたこと Haskell Haskellで書かれたプログラムをマイコンで動かすことができると某界隈に衝撃を与えたAjhcですが、FreeBSD機にインストールする時に躓いた事が有りましたのでまとめておきたいと思います。 続きを読む