2011-01-01から1年間の記事一覧
もう2011年も終わりなので、参加したイベントを中心に、今年を振り替えってみたいと思います。 今年もいろんなことがありました。 1月: /usr/bin消失 年明け早々、/usr/binを消しました。 そして、iMacが壊れて、SnowLeopardのディスクを飲み込まれました。 …
# この記事は名古屋クリスマスハッカソン2011で書いてます。メリークリスマス!GistとかTwitterとかの最近のWebサービスは他のページに埋め込めるようになっていますね。ただ、サービスごとに埋め込むためのHTMLコードが違うので、いちいち調べるのが面倒です…
(* この記事は、F# Advent Calendar 2011の16日目の記事です。 *)こんにちは、mzpです。 クリスマスたのしみですね。 さて、関数型プログラマは自分だけの関数を持っていることが多いものです。 ライブラリ化にするほどの規模でないので、コピペによって各プ…
(* この記事はTheorem Proving Advent Calendar 2011の5日目の記事です。 *)Coqはタクティックを使って対話的に証明を構築していけます。その反面、注意して書かないと、読みにくい証明になってしまいます。 そんなときは、Show Scriptコマンドで整形すると…
11/5にLL名古屋というイベントを開催されました。 プログラムを見てもらえば分かりますが、いわゆるLLではなく「Lが2個はいっていれば、それはLLです」がテーマのLT大会でした。 開催経緯 発端 OSC Nagoya 2011とLL Planetの開催日が同日だったせいでLL Plan…
Gallinaによる証明駆動開発の魅力 View more presentations from Hiroki Mizuno
id:yoshihiro503さんに誘われて、VSTTE Competitionというソフトウェア検証コンテストに参加しました。 「検証ツールに特に制限はないぜ」と書かれていたのでCoqを使いました。競技プログラミンングに初めて参加しましたが、48時間ぶっとうしで同じ課題に取…
ProofSummit2011でMsgPackを証明したときの話をしてきました。内容は名古屋Reject会議で話したことを膨らませた感じになっています。 話の趣旨としては「バグって怖いじゃん → じゃあ証明しようぜ → やってみた」みたいな感じです。 スライド CoqによるMsgPa…
git + Redmineで開発する場合、Redmineのチケットごとにトピックブランチを切ることが多いですが、ちょいちょいチケットの内容を忘れてしまいます。 そういうときに、いちいちブラウザでチケットを見にいくのがダルいので、チケットのサマリを表示するgitの…
追記: 公式プラグインになりました。Websocket Plugin - Jenkins - Jenkins Wiki 「pollingが許されるのは小学生までだよねー キモーイ キャハハハハハハ」というわけでビルド結果をpush通知するJenkinsプラグインを書きました。 特徴 Jenkinsのビルド結果を…
@akinekoさんの勉強会を開催or参加する人が気をつけたい11のこと - Akinekoの日記に影響されて、ボクが勉強会を開くときに気をつけてることを書いてみます。 いままでにやった勉強会 partake.in 勉強会の方針 気楽に開催できて、気軽に参加できるゆるい勉強…
東京で「partake.in」を主催してきました。「東京の勉強会にも一度は参加したいなー」と前から思ってましたが、まさか主催することになるとは思ってませんでした。会場の手配等々は@7shiさんに頼りっぱなしでした。ありがとうございます。「Flashのバイナリ…
くえにしさん([twitter:@kuenishi]さん)に誘われたのでMessagePackハッカソンに参加してきました。 MessagePack本体のレポジトリにMessagePack for OCamlを取り込んでもらったので、みんな使ってください! MessagePackって? JSONやYAMLと同程度の表現能力を…
証明駆動開発のたのしみ@名古屋reject会議 View more presentations from Hiroki Mizuno
Coq to Rubyによる証明駆動開発@名古屋ruby会議02 View more presentations from Hiroki Mizuno
名古屋Ruby会議02のとなりで名古屋Reject会議というイベントを開催してきました。 「Rubyという言葉を使ったら負け」みたいな雰囲気のある謎なイベントでした。たのしかった!当日は[twitter:@maeda_]さんがustream中継を、[twitter:@wof_moriguchi]さんがタ…
最近、[twitter:@suer]、[twitter:@mallowlabs]、[twitter:@shimomura1004]と夜な夜なSkypeでチャットしながらソフトウェア開発をしてるんですが、だんだんとSkypeチャットの機能に対する不満が溜ってきました。 というわけで、Skypeチャットをリプレースす…
http://twitpic.com/3w34bo はじめに モナドといえばHaskell、Haskellといえばモナドが有名ですが、モナドは特定の言語とは無関係の仕組みですので、F#でも使えます。ただ単に使えるだけでなくコンピュテーション式というモナドをより便利に使うための文法ま…
WebSocketって何? WebSocketは、Javascriptでサーバとリアルタイム双方向通信をする仕組みです。概要は第1回 WebSocket登場までの歴史:Jettyで始めるWebSocket超入門|gihyo.jp … 技術評論社によくまとまっています。この記事ではWebSocketサーバを実装しな…
先日の1/17に/usrを消してしまいました。正確には、カレントディレクトリにできたusrディレクトリを移動させようとして、うっかり/usrを移動させてしまいました。 /usr消失→状況確認(22:30ごろ) frama-cをインストールしようとして、/usrを消してしまう。Sky…
実践 F# 関数型プログラミング入門作者: 荒井省三:いげ太出版社/メーカー: 技術評論社発売日: 2011/01/07メディア: 大型本購入: 6人 クリック: 264回この商品を含むブログ (26件) を見るいげ太さんに献本をいただきました。ありがとうございます! 感想として…