あけましておめでとうございます。今年もよろしくお願いします。 Coqのモジュール関連の機能について和訳したので基本的な機能を紹介します。 リファレンスの文中で「対話的」モジュールとされているのは Vernacular を使って定義するからで、実体は Structu…

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

ガリグ先生の講義の9番目の資料(ssrcoq9.v)で出てくる bigop について、mathcomp.ssreflect.bigop の冒頭を訳しました*1。ssrcoq9.v の中では Notation であるはずの \big[op/idx]_～ が Definition になっていたりして混乱しますが、直接定義だけを追うより…

最近 coqtokyo 第7回Ssreflect勉強会 に参加しています。 隔週で火曜日にやっているので是非。 もうすぐ第五回講義資料(ssrcoq5.pdf)に到達しますが、ここでようやく mathcomp の話が出てきます。 さっそく opam で mathcomp をインストールしようとしたとこ…

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

ProofSummit2017とML勉強会#2に参加してきました。 とりあえず二日連続はつらいものがあった。 個々の感想 SML#の話は良かった。言語や処理系の機能が列挙されていると個人的に楽しい。そういう意味ではATSも楽しいんだけど、機能(のアップデート)が少なかっ…

遅めの夏休みを使ってProofSummit2014とJSSST2014に行ってきました。Coqチュートリアルとサマースクール(スパコンの話)に参加し、火曜日のPPLとその他セッションをふらふらしてた感じ。 Coqチュートリアルが主目的で参加したハズなんですが、謎の強烈な眠気…

8/25,26でなにやらイベントが連続していたので行ってきました。 ProofSummit2013 OCamlMeeting2013 なごやまつり 後続のせいでかなり地味な印象になってしまったけど(^^、聴いて意味があったのは前半。 OCamlSummit 期待していた Generic Pretty Printer は…

Coqチュートリアル#4最終回に行って来ました。4回とも参加できたので皆勤賞です！ 講師の [twitter:@tmiya_] さんと運営の [twitter:@kenkoba] さんお疲れ様でした。 window.twttr = (function(d, s, id) { var js, fjs = d.getElementsByTagName(s)[0], t =…

気になっていたところに Formal Methods Forum主催Coqチュートリアル＃1があったので、どんなもんかと聞いてきました。 当日の資料もリンク先に挙がってますね。 受講者は8人くらい？来てました。 Formal Methods Forumの @tmiya_ さんが主に解説して @kenco…