2011-01-01から1年間の記事一覧

2011年の振り替えり

もう2011年も終わりなので、参加したイベントを中心に、今年を振り替えってみたいと思います。 今年もいろんなことがありました。 1月: /usr/bin消失 年明け早々、/usr/binを消しました。 そして、iMacが壊れて、SnowLeopardのディスクを飲み込まれました。 …

Webサービスの埋め込み用HTMLを手軽に取得するためのWebAPI『QuoteIt』を作りました

# この記事は名古屋クリスマスハッカソン2011で書いてます。メリークリスマス!GistとかTwitterとかの最近のWebサービスは他のページに埋め込めるようになっていますね。ただ、サービスごとに埋め込むためのHTMLコードが違うので、いちいち調べるのが面倒です…

ちょっと便利な関数の紹介

F#

(* この記事は、F# Advent Calendar 2011の16日目の記事です。 *)こんにちは、mzpです。 クリスマスたのしみですね。 さて、関数型プログラマは自分だけの関数を持っていることが多いものです。 ライブラリ化にするほどの規模でないので、コピペによって各プ…

Show Scriptコマンドによる証明の整形

Coq

(* この記事はTheorem Proving Advent Calendar 2011の5日目の記事です。 *)Coqはタクティックを使って対話的に証明を構築していけます。その反面、注意して書かないと、読みにくい証明になってしまいます。 そんなときは、Show Scriptコマンドで整形すると…

LL名古屋 開催経緯

11/5にLL名古屋というイベントを開催されました。 プログラムを見てもらえば分かりますが、いわゆるLLではなく「Lが2個はいっていれば、それはLLです」がテーマのLT大会でした。 開催経緯 発端 OSC Nagoya 2011とLL Planetの開催日が同日だったせいでLL Plan…

LL名古屋 発表資料『Coq/GaLLinaによる証明駆動開発の魅力』

Gallinaによる証明駆動開発の魅力 View more presentations from Hiroki Mizuno

VSTTE Competition参加記録

id:yoshihiro503さんに誘われて、VSTTE Competitionというソフトウェア検証コンテストに参加しました。 「検証ツールに特に制限はないぜ」と書かれていたのでCoqを使いました。競技プログラミンングに初めて参加しましたが、48時間ぶっとうしで同じ課題に取…

ProofSummit 2011 で『CoqによるMsgPackシリアライザの証明と実装』という話をしました。

ProofSummit2011でMsgPackを証明したときの話をしてきました。内容は名古屋Reject会議で話したことを膨らませた感じになっています。 話の趣旨としては「バグって怖いじゃん → じゃあ証明しようぜ → やってみた」みたいな感じです。 スライド CoqによるMsgPa…

gitとRedmineと連携させるgitサブコマンド: git-ticket

git + Redmineで開発する場合、Redmineのチケットごとにトピックブランチを切ることが多いですが、ちょいちょいチケットの内容を忘れてしまいます。 そういうときに、いちいちブラウザでチケットを見にいくのがダルいので、チケットのサマリを表示するgitの…

Jenkinsのビルド結果をリアルタイム通知するプラグイン『Jenkins Websocket Notifier』を作りました

追記: 公式プラグインになりました。Websocket Plugin - Jenkins - Jenkins Wiki 「pollingが許されるのは小学生までだよねー キモーイ キャハハハハハハ」というわけでビルド結果をpush通知するJenkinsプラグインを書きました。 特徴 Jenkinsのビルド結果を…

ゆるい勉強会の開き方

@akinekoさんの勉強会を開催or参加する人が気をつけたい11のこと - Akinekoの日記に影響されて、ボクが勉強会を開くときに気をつけてることを書いてみます。 いままでにやった勉強会 partake.in 勉強会の方針 気楽に開催できて、気軽に参加できるゆるい勉強…

「ActionScriptを使わないswf勉強会 #1」を開催しました

東京で「partake.in」を主催してきました。「東京の勉強会にも一度は参加したいなー」と前から思ってましたが、まさか主催することになるとは思ってませんでした。会場の手配等々は@7shiさんに頼りっぱなしでした。ありがとうございます。「Flashのバイナリ…

MessagePack for OCamlを公開しました

くえにしさん([twitter:@kuenishi]さん)に誘われたのでMessagePackハッカソンに参加してきました。 MessagePack本体のレポジトリにMessagePack for OCamlを取り込んでもらったので、みんな使ってください! MessagePackって? JSONやYAMLと同程度の表現能力を…

名古屋Reject会議で「証明駆動開発のたのしみ」というタイトルで発表してきました

証明駆動開発のたのしみ@名古屋reject会議 View more presentations from Hiroki Mizuno

名古屋Ruby会議で「Coq to Rubyで初める証明駆動開発」というタイトルで発表してきました

Coq to Rubyによる証明駆動開発@名古屋ruby会議02 View more presentations from Hiroki Mizuno

名古屋Reject会議を開催しました

名古屋Ruby会議02のとなりで名古屋Reject会議というイベントを開催してきました。 「Rubyという言葉を使ったら負け」みたいな雰囲気のある謎なイベントでした。たのしかった!当日は[twitter:@maeda_]さんがustream中継を、[twitter:@wof_moriguchi]さんがタ…

開発者用Webチャットシステム『AsakusaSatellite』をリリースしました

最近、[twitter:@suer]、[twitter:@mallowlabs]、[twitter:@shimomura1004]と夜な夜なSkypeでチャットしながらソフトウェア開発をしてるんですが、だんだんとSkypeチャットの機能に対する不満が溜ってきました。 というわけで、Skypeチャットをリプレースす…

F#プログラマのためのMaybeモナド入門

http://twitpic.com/3w34bo はじめに モナドといえばHaskell、Haskellといえばモナドが有名ですが、モナドは特定の言語とは無関係の仕組みですので、F#でも使えます。ただ単に使えるだけでなくコンピュテーション式というモナドをより便利に使うための文法ま…

サーバを作りながら学ぶWebSocketプロトコル

WebSocketって何? WebSocketは、Javascriptでサーバとリアルタイム双方向通信をする仕組みです。概要は第1回 WebSocket登場までの歴史:Jettyで始めるWebSocket超入門|gihyo.jp … 技術評論社によくまとまっています。この記事ではWebSocketサーバを実装しな…

MacBookAirの/usrが消失した件

先日の1/17に/usrを消してしまいました。正確には、カレントディレクトリにできたusrディレクトリを移動させようとして、うっかり/usrを移動させてしまいました。 /usr消失→状況確認(22:30ごろ) frama-cをインストールしようとして、/usrを消してしまう。Sky…

『実践F#』レビュー

実践 F# 関数型プログラミング入門作者: 荒井省三:いげ太出版社/メーカー: 技術評論社発売日: 2011/01/07メディア: 大型本購入: 6人 クリック: 264回この商品を含むブログ (26件) を見るいげ太さんに献本をいただきました。ありがとうございます! 感想として…