なつやすみのにっき

夏休みです。

Coq Summer School

8月の終わりに NII Shonan School on Coq に行ってきました。

f:id:amutake:20140829120638j:plain

一週間みっちりCoq漬けでした。楽しかった。でも英語ができればもっと……。

夏ゼミ

Coq合宿が終わった3日後から2泊3日の研究室合宿がありました。千葉の館山に行きました。

1,2日目はずっとゼミでした。ものすごく疲れた。自分は Coq School でどんなことを学んできたかについて発表しました。

最終日はみんなで鋸山に行きました。

f:id:amutake:20140903114445j:plain

下の写真は帰りのフェリー。予想以上に良かった。また乗りたい。

f:id:amutake:20140903142400j:plain

幹事として至らないところもありましたが無事に終わって良かったです。ありがとうございました。

あと酔った同期がめちゃくちゃおもしろかったです。普段もあんな感じでいればいいのに……。

ProofSummit2014 & JSSST2014

夏ゼミの3日後から名古屋でした。ProofSummit -> Coq/SSReflect チュートリアル -> JSSST という順番。

ProofSummit

ProofSummit2014でLTをしました。 内容は ProveEverywhere についての宣伝です。

ProveEverywhere というのは僕が Android アプリを作る授業で作ったアプリで、CoqIDE を真似たものです。

Coq をスマホで動かすアプリはいくつかありますが、それらは Coq をアプリにまるごと入れています。これは coqtop サーバを別に用意するので軽かったりします。

(この発表の時点ではリポジトリhttps://github.com/amutake/prove-everywhere にあったのですが、関係するディレクトリとかリポジトリが増えてきたので https://github.com/prove-everywhere に移行しました)

Coq/SSReflect チュートリアル

Affeldt さんによる Coq と SSReflect/MathComp のチュートリアルです。

正直、誰でもわかるような簡単で、ちょっと触ったことがある人なら退屈な内容になるんだろうな〜と思っていましたが、全くそんなことはなかったです。とても濃いチュートリアルでした。

この資料 (https://staff.aist.go.jp/reynald.affeldt/ssrcoq/) は全 Coq ユーザーが読むべきだと思います。

JSSST

日本ソフトウェア科学会の全国大会です。最終日の Coq セッション (Coq のみのセッション!!) で発表しました。

外で研究について発表するのはこれが初めてだったのでものすごく緊張しましたが、無事に(?)終わって良かったです。

いま

今は BIGCHA というのに参加しています。Hadoop を使ってなんかアプリを作ろうというやつです。言語は30億のデバイスで走るという噂のジャバです。

ジャバのコードを見ていると頭が痛くなる病気になってしまいました。

おわり

おわり。

追記

今気づいたけど BIGCHA 以外すべて Coq 関係だった