日記

Prattパーサの記事を読んだ

Rustで追実装しながら zenn.dev を読みました。 頭から読んでいけば分かる丁寧な説明だったため思ったより理解に時間は掛かりませんでした。 ただmixfix operator(そんな分類はこのアルゴリズムには無さそうだが)のbinding powerについてはもう少し説明が欲…

プログラミング言語の形式的意味論入門を買った

プログラミング言語の形式的意味論入門 を買いました。 表紙に書いてありますが The Formal Semantics of Programming Languages: an Introduction という洋書の和訳です。 多分途中で挫折しますが、とりあえず頭から眺めてみようと思います。 エラッタ 見つ…

sigplanブログにMPLの記事が投稿されていた

並列MLであるMPLについての記事がsigplanのブログに投稿されていました> Provably Space-Efficient Parallel Functional Programming | SIGPLAN Blog。 面白いし論文より分かり易いので読みましょう。 MPLはSMLに並列計算のための機能を追加した並列MLの一つ…

CoqのマニュアルのTermの章を翻訳した

Coq v8.8.2 の Term の章を翻訳しました。 この章では Gallina の項の構成について説明しています。 恐らくトピックとして一番難しいのは依存型を扱うマッチ式についての説明で、詳細は別のページに独立してるくらいですが、この章で示されている例は簡潔な…

MDN の JavaScript building blocks を読み終えた

前回 に引き続き JavaScript の構成要素 を読みました。 if, for, while, イベント, イベントリスナ、イベントハンドラ などが導入されました。 文中の練習問題はテキストエリアに入力されたコード片がインタラクティブにその場に反映されるというものなので…

MDN の JavaScript First Steps を読んだ

JavaScriptを勉強することにしました。 ECMAScriptという名前で呼ばれていない時点で気にくわないものであることは確定なんですが、学ぶのが妥当という判断になってしまいました。まずMDNのJavaScriptの第一歩という教材を一通り読んで課題をやりました。 Ja…

coqdocを使った

coqdocを初めて使ってみました。はじめは company-coq のスタイルに合わせて見出しとか書いてましたが、なんとなく気が向いたので公式(documenting-coq-files-with-coqdoc )の方を確認してみたのでした。目的はcoqスクリプトの(主にコメントの)整形スタイル…

RustでマルチスレッドWebサーバを作る例を写経

Final Project: Building a Multithreaded Web Server - The Rust Programming Languageを写経した。 標準ライブラリのみを使って簡単なマルチスレッドWebサーバを書く例。 スレッドプールを作ってacceptするたびに「htmlを応答する関数」をJobとしてチャン…

歯が痛くて倒れていた

8月中旬頃、突然奥歯(の中の神経)に激痛が起こりました(結局明確な原因は不明)。 2週間くらいしてようやく普通の生活が出来るようになりました。あまりに酷い状態だったので書き留めておきます。 どんな状態だったかというと: 常に痛い。何もして無くても神…

terraformのチュートリアルを読んだ

terraformのチュートリアルを一通り読んで実行した。 チュートリアルを実行するのに必要な知識が全てチュートリアル内にあり、かなり分かりよい ほぼ写経で動く(1度AWSのよく分からないエラーが出たけど) 記述が古い箇所がある(動きはする) その時点でのconf…

静的コード解析の会 第0回 でVeriFastについて発表してきた

#静的コード解析の会 第0回でC言語(とJava)の検証器であるVeriFastについて発表してきました。資料は公開してあるので興味ある人は見てください。動画もあります。 > https://metasepi.connpass.com/event/42141/presentation/ 結構(私の理解が)きわどい質問…

DeBruijn変換がやっと分かった

算譜工論(DeBrujn変換) を読んでDeBruijn変換をSMLで実装してみました。> https://gist.github.com/eldesh/5714388 文書内の説明がほとんどMLのコードまんまなのでほとんど単なる写経なのですが。 ちなみに、これによってどんな嬉しい性質があるのかはまだ…

JAXA H-IIB打ち上げ成功(したみたい)

ライブ中継観てた. なんで今回はあんなにテンション高く観てたのか謎. ニコニコ生放送は定員オーバーでNice boat.された. 有料会員の人は見られてたのかな. ついでにirc.friend-chat.jpも落ちてた. 珍しい.

はてなerになりました

日記のタイトルは悩むなー. とりあえず右往左往と読むということでよろしくw