動機 昔、モータードライバを自作しようと試みた事がありました。しかし、自作のドライバはロボコンで用いられていた既製品に対して信頼性で劣っており、既製品の出力に不満が無かったために置き換えられませんでした。

学校の課題でガウスの消去法を実装しました。言語は特に指定されなかったのでOCamlです。

EvalML1Errにおける評価の全域性の証明でML1*1のすべての式に評価される値が存在することが分かったので、式を評価する関数書いてみたいと思います。また、せっかくCoqで書いたので関数が妥当であるかの証明とOCamlソースコードの出力も行おうと思います。 *…

前回、前々回は四則演算程度しか持たない導出システムについての証明でしたが、今回は変数束縛や環境を持つ導出システム、EvalML2における評価の一意性を証明しようと思います。例によって元ネタはプログラミング言語の基礎概念です。

Haskellで書かれたプログラムをマイコンで動かすことができると某界隈に衝撃を与えたAjhcですが、FreeBSD機にインストールする時に躓いた事が有りましたのでまとめておきたいと思います。

前回はプログラミング言語の基礎概念に出てくるEvalML1についての定理を証明したので、ついでに実行時エラーも扱うEvalML1Errにおける評価の一意性を証明したいと思います。

Coqの練習にプログラミング言語の基礎概念に出てくる、EvalML1における評価の一意性について証明したので公開したいと思います。

タイトルの通り、OCamlでOCamlのサブセットの型推論を書いたので、その事について纏めておこうと思います。

プログラミング言語の基礎概念と言う意味論や型理論の入門に良さげな本が有るんですが、この本は嬉しいことにオンライン演習システムが有るので実際に手を動かしながら内容を理解することができます。

過渡応答を求めるのって正直面倒臭いですよね！電気系の学生には多分頷いてもらえると思います。 中でも面倒臭いのは正弦波が入力された時。微分方程式を直接解くにしても難しいし、ラプラス変換するにしても部分分数展開するにしても面倒臭い困ったやつです…