残業プログラマのためのスキルアップリンク集

お知らせ:内容がばらばらになったので、ネットで学ぶソフトウェア工学に一部移しました。

もくじ

プログラミング

プログラミング言語 関数型言語 Haskell Lisp Ocaml ML F# SICP プログラマ

検証

QuickCheck Coq モデル検査 形式手法 CSP

そのほか

ツール コンテスト 関数型言語使用の企業 研究室 学会 プログラミング系のブログ
更新ログ
『プログラマのためのWEB』に戻る


プログラミング言語

『プログラミングの基礎 (Computer Science Library)』

プログラミングの基礎をOCamlで解説。特定のプログラミング「言語」の基礎を教える本は多くあれど、「プログラミングの基礎」を語る本は少ない。この本は数少ないその一冊だろう。プログラミングを始める人にまず薦められる本だ。丁寧で、プログラミング初心者にもってこい。全部で270ページあるのだが、175ページめ引用「本の半ばを過ぎたところで最初の完動プログラムを作ることができました。皆さんはすでに立派なプログラミングの中級者です。」とある。なにっ?唐突に中級者になれるのだ(笑)しかし、笑ったけど、ほんとにそうかもしれないと思う。なぜなら、この本は関数型言語の機能を使ったり、デザインレシピという道具を使ったりして、プログラミングの作り方の基本がしっかり身につけられるようになっている。この本を読んだ読者からすると、多くのプログラマがあまりに基本を身に着けていないことに気づくだろう。プログラミング言語の入門書を何冊か読んだだけのビギナーより、この本の読者のほうが数段上の力がある、とぼくには思える。そして、第24章「まとめ -プログラミングとは-」の264ページも引用。「本書を読み終えた皆さんはプログラミングの上級者であるばかりでなく、すでにOCamlの上級者でもあります。」プログラミングの基礎を勉強しているはずが、いきなり上級者になって、しかもOCamlの上級者になってしまった!wwwww。ドラゴンボールの亀仙人の修行か!(笑)ちょっと大げさだけど、すごくいい本なんだ。ぼくがだれかにプログラミングを教えるとしたら、この本を使うだろう。もっと早くこの本が出版され、学生時代に読んでいたら、と思う。ぜひ、みんなに読んでもらいたい。もっと早くこの本が出版され、学生時代に読んでいたら、と思う。ぜひ、みんなに読んでもらいたい。
プログラミング言語研究への誘い
「職人プログラマ」と「ソフトウェアの専門家」の差とは?
百年の言語 --- The Hundred-Year Language
プログラミング言語に力の差はあるのか?
言語の世界
Ruby作者まつもとゆきひろによる
どう書く?org
お題をいろんな言語で実装して、投稿するサイト
TIOBE Software: Tiobe Index
プログラミング言語ランキング。検索エンジンの検索数から算出。
僕やはてながPerlを選ぶ理由 2005-05-18 - naoyaのはてなダイアリー
引用「そんな僕の物作りの過程においては、コンパイラにやたらと怒られたり、変数の型を気にしたり、変数に入れるオブジェクトが何者だったりするかをいちいち意識しなければならない静的型付けの言語は性に合わなかったんですね。一方で簡単なことは簡単に、難しいことでもそれなりにできる Perl という言語は、僕のやり方に合っていたし、なんとなく"Hackしている"という気分にも浸ることができたんです。」。ちょっと動的型付け、静的型付けって問題かは、わからないな。Haskellでもハックしてる気になれるけどなあ。
プログラミング言語ヒエラルキー

関数型言語、関数型プログラミング

なぜ関数プログラミングは重要か
「関数型言語」に関するFAQ形式の一般的説明(on demandに加筆修正します) - Qiita
東北大学の住井先生による関数型言語の解説。
関数型言語 - 関数型プログラミング言語の定義&実装の仕方の例 - Qiita
同じく住井先生。
なぜ次に学ぶ言語は関数型であるべきか
Ocamlで具体的に説明されています。これだけではない気もする。
『関数プログラミングの楽しみ』
まだ読んでないけど、時間をつくって読みたいな。
関数型言語の技術マップ
Ladder of Functional Programming 〜関数型プログラミングのレベル分け〜
私はAdvanced Beginnerぐらいかな。
関数型言語を独学で勉強している学生です への答
遅延評価ってなんなのさ
Functional Jobs // Dream Jobs for Functional Programmers
関数型言語プログラマのための求職情報。関数型言語って範囲で共有している知識(ラムダ?)があるから、こういうサイトができる。それはすばらしいことだと思う。
ATSプログラミング入門
TBD。依存型とか関係ありそう。
Try F#
ブラウザ上で、F#を実行し、学習できるよう。
ニコニコ生放送の配信基盤改善
Erlangの話。
JavaScript で Lisp の処理系 (と REPL) を実装してみた - mooz deceives you
JavaScriptで読む「ラムダ計算基礎文法最速マスター」 - 貳佰伍拾陸夜日記
MiSPLi
small lisp implementation written in javascript
The Implementation of Functional Programming Languages - Microsoft Research
Simon Peyton Joneによる著作のPDF。

Haskell

プログラミングHaskell 第2版
モナドの説明が、ファンタク、アプリカティブ、モナドと自然な感じでわかりやすい。本質をついて、かなりセンスが良さそうな本。2021年に読んでいます。
Learn You a Haskell for Great Good!
英語か、あとでまたよむ。と思ったら、日本語訳が出版された。読了した。非常に良い本だった。初心者にすすめるなら断然これだ。カジュアルで読みやすく本質をついた説明だった。ぼくの読んだ感想:すごいHaskellたのしく学ぼう!: Miran Lipovačaをもっと早く読めばよかった: プログラミングは眠るのも忘れてすごいH本、1回目読み終わって、よかったから、2回目の復習に入った。: プログラミングは眠るのも忘れて。それと、他のHaskeller(多分有名な人)の書評:「すごいHaskellたのしく学ぼう!」は気配りと楽しさがすごい - keigoiの日記すごいHaskellたのしく学ぼう! - あどけない話がいいかな。あと、ここすごいHaskellたのしく学ぼう!を読んだ - south37の日記たしかに丁寧な本だよね(翻訳も含めて)。間違いもないし、ぼくは非常に丁寧な仕事と見ました、本の構成、内容について。ということで、良本であり、労作であると言いたい。
『すごいHaskellたのしく学ぼう!』
M.Hiroi's Home Page / Haskell Progamming
お気軽らしいです。説明が丁寧でいいですね。昔の記事なので現在ではコンパイルが通らないこともあります。
Try Haskell! An interactive tutorial in your browser
ブラウザ上でHaskellをちょっといじれる。IE非対応?
モナモナ言わないモナド入門
Haskellといえば、モナドが一つの壁ですね。『プログラミングHaskell 2nd』(上述)とか『すごいH本』でまずは勉強するといいと思います。
モナド変換子(その1: 基本)Qiita
短め。モナド変換子の理解に事前知識は必要ですね。ライブラリ使用でモナド変換子の理解が必要になることがある。いつかは超える山。
Haskell モナド変換子 超入門
長め、けっこうわかりやすい。sapou.orgの説明も昔からある。説明も進化していくもんですね。
モナド変換子 お気楽 Haskell プログラミング入門
QAで学ぶMonad - あどけない話
Haskell - Wikibooks, open books for an open world
wikiでの解説、結構マニアックなところまで行けるかも。日本語の翻訳は追いついていない部分が多いですね。英語で読もう。でも品質は不明。wikiだし。
Parallel and Concurrent Programming in Haskell
並行、並列プログラミングをHaskellで。オンライン版をフリーで読めるっぽいです。
24 Days of GHC Extensions
GHC拡張は抑えておくとよいよな。real world haskellだって入門書なのにGHC拡張の紹介あるし。まあほとんどないんだけど。おいらはまだ理解していないから理解したくて型システムの興味をそそるのもいいよね。型システムだって趣味として勉強するのもいいし登っていく山(どれだけ高いかはよくわからない)としてもいいだろうね。暇つぶしに読むのももちろん可。
「タイプセーフプリキュア!」を支える技術
GHCの言語拡張についてちょっと勉強できます。
48時間でSchemeを書こう
HaskellでScheme(Lispの方言)を実装する。勉強になる。
Higher Rank Type とは
RankNTypesの一例による説明。わかいやすい。こういうちょっとした説明がありがたい。Wikibookよりとっかかりはよいな。
extensible チュートリアル 1
ここもRankNTypesを使っている。そもそもTry PureScript! Type Classesをみてたんだっけか。
Haskell/Polymorphism - Wikibooks, open books for an open world
STモナドの部分が不明。STモナドはなぜ変更可能な参照を外へ持ち出せないのか調べてみた - shinharadの日記に説明がある。Wikiだけあって工事中もあるし、説明不足もあるのか。forallの説明重複している気がするし。
やさしい Haskell 入門 (バージョン98)
WEBで始めるならここか。
『ふつうのHaskellプログラミング』
わかりやすい入門書。遅延評価などをおさえており、関数型言語の楽しさに入門できる。モナドは説明が不足している。
GADTs使ってみた - Faith and Brave - C++で遊ぼう
GADTsのわかりやすい説明だ。
GADTsは、データコンストラクタを型付けすることができる代数データ型です。これによって、従来のあらゆるデータコンストラクタを許可する関数を定義できるだけでなく、特定のデータコンストラクタのみを許可する関数を定義できるようになり、さらなる柔軟性と、実行時エラーに対するさらなる強い保証を手にすることができるようになります。
01. GADTs - とりあえず雑記帳
Phatom typeとその限界を説明した後にGADTsでの解決策を説明した。わかりやすい。
定理証明系 Haskell - konn-san.com
Haskellの型システムで定理証明する話?型の不変条件が定理なのかな。それを種(kind)で表現する。定理の証明はsingletonを使う。
DataKinds 拡張は、上のように定義した代数的データ型を型レベルに持ち上げることが出来る言語拡張である。より厳密には、Nat型を種レベルに持ち上げたNat種と、その種に属する型コンストラクタZ :: NatおよびS :: Nat -> Nat がGHCによって自動的に定義されるようになるのだ。これらは全く同型なものであるため、あたかもNatデータ型の値が、型レベルに昇格されたように見える訳である。これを使えば、先程のベクトルの例は次のように書き直せる:
途中で終わって中途半端かな。
「アルゴ式」をHaskellで学ぶための準備
競技プログラミングに興味がでたので。配列の書き換えとかどうやってやればいいのかな、とか。
Haskellで競技プログラミング
これも。
AtCoder に登録したら解くべき精選過去問 10 問を Haskell で解いてみた - Qiita
Haskell における依存型プログラミングと証明の記述を用いた実用的なプログラミングって何 - Togetter
上のリンクと同じ話者。Haskellの型システムで定理証明する説明。だけど難しいな。
Dependently typed programming and theorem proving in Haskell | Wolfgang Jeltsch
定理証明の簡単な事例まで紹介している。
Haskellにおける型レベルプログラミングの基本(翻訳) - Qiita
あとで理解する。
Part I: Dependent Types in Haskell - School of Haskell | School of Haskell
あとで理解する。
CS240h: Functional Systems in Haskell
スタンフォード大のHaskellの授業。Phantomとか。
Haskell アクション 超入門 - Qiita
Haskellと副作用の話。こんなに解説が乱立するとは。説明がたくさんあるってどういうことだろう。難しいってこと?
副作用の話 - モナドとわたしとコモナド
Haskellと副作用の話。
HaskellのモナドIO - HaHaHa!(old) - haskell
Haskellと副作用の話。ちょっと古い。
Haskellには副作用がないのか? - あどけない話
Haskellと副作用の話。
Haskell の Monad とは言語内DSLのフレームワークである - あどけない話
Haskellと副作用の話。じゃなかったか。。。
HRR: Quick start
DB操作系?SQL系のHaskellライブラリらしい。
Extending Query, Relational, Typeful, Composable - khibinoの日記
HRRの説明?
GHC(STG,Cmm,asm) illustrated for hardware persons
Haskellの代表的コンパイラGlasgow Haskell CompilerことGHCのアーキテクチャとか解説。
xmonad | the tiling window manager that rocks
キーボードだけでがんばれるウインドウマネージャーらいいです。BSDとLinuxしかないぽい。
Haskell-mode for Emacs
Emacs用のHaskell開発環境。
本物のプログラマはHaskellを使う
Yesod Web Framework for Haskell
HaskellのWebフレームワーク。Yesodを勉強すると、自分のHaskell世界が広がります。モナドを勉強しないといけないし。
Web アプリケーション・フレームワークYesod
山本和彦さんの説明資料。参考:Mighty and Yesod。Mightyなにかしらんですけど。
Yesod勉強会『HaskellとWeb開発』
田中英行さんの説明資料。
(祝) Yesod 1.0 勉強会
Haskell web programming A Yesod tutorial
Yesodを支える技術
Haskellが使えるホスティングサービス @ val it: α → α = fun
できる!Template Haskell
Pandoc a universal document converter
Haskellで書かれたドキュメントフォーマットのコンバータ。マークダウン記法からHTMLのスライドショーが作れるのがいいね。texとかにもなるよ。「If you need to convert files from one markup format into another, pandoc is your swiss-army knife.」
モナドのすべて
Haskell - Wikibooks, collection of open-content textbooks
どっぐらいふ・ろぐ
HDBC-sqlite3の使い方など。cabelでインストールする必要もあるよ。
Haskell で OAuth API利用Tweetしてみた - HaskellでTwitterクライアント開発blog(仮)
twitter関係では、OAuthの使い方もコードにべたっと書いてあって、勉強になる。
Conduit で Twitter Streaming API を扱う - KrdLab's blog
Haskellのコード150行で, Twitterに投稿するだけのクライアントを作ったよ - プログラムモグモグ
うえにコードが似てる。あまり参考にしていない。
HaskellでOAuthとTwitter API - kenkov diary
Haskell で OAuth - EAGLE 雑記
作ってみよう Enumerator - http-enumerator で Twitter API ぺろぺろ - ごったく
haskell で twitter の timeline を取得してみる - プログラマのネタ帳
hs-twitterって、ライブラリは結局、使えないぽい。あまり参考にならないか。
haskellでtwitter APIを使う - tsurushuuの日記
古い時代の言語設定を読む例。JSONの扱い方は参考になるかも。
HaskellでTwitterにpostする - yunomuのブログ
Web.Authenticate.OAuthとか使って、エレガントだけど、WEBアプリだったら、どう使うのか、不明。
HaskellでRSSを読み込む
HaskellでFTPクライアント | hippos-lab::blog
本物のプログラマはHaskellを使う - 第39回 一般向けの「Haskell Platform」とインストール・ツールの「ca...:ITpro テキストI/OのUnicode対応
文字化けに悩まされることがあります。未熟じゃ。
windowsでHaskellのIOまわりで日本語を文字化けなく表示させる方法 - プログラミングお勉強きろく
これも文字化け参考めも。
Haskell のお勉強
「まとまった日本語の解説がほとんど無いので、 簡単な解説記事を書いてみました。」とのこと。
CS240h: Functional systems in Haskell
stanford.eduの授業?
EclipseFP
Haskell開発環境のEclipseプラグイン。コンテンツ・アシスト、コンパイルエラー検知。Eclipse自体、最近重いから、つかってない…
Haskell 脳の恐怖
ネタ。

OCaml

『プログラミング in OCaml ~関数型プログラミングの基礎からGUI構築まで~』
数理科学的バグ撲滅方法論のすすめ
東北大学の住井先生による連載。未読。Ocamlで説明してあるらしいのでここに分類。
Try OCaml
ブラウザ上で、OCamlを実行し、学習できるよう。
Js_of_ocaml
「Js_of_ocaml is a compiler of OCaml bytecode to Javascript. It makes it possible to run Ocaml programs in a Web browser.」
ウェブブラウザで関数型プログラミング! js_of_ocaml
Ocamljs
開発止まっているぽいです。「Ocamljs is a system for compiling OCaml to Javascript.」
ocamljs を使おう : OCamlからJavaScriptへの変換
型付きWebフレームワークで遊んでみた // Speaker Deck
OCamlのWeb FWの話。
OCaml toplevel
Web上のOCaml処理系
Effective ML 9ヶ条

ML

プログラミング言語SML#解説
C言語とのシームレスな連携などが特徴ときいております。
『プログラミング言語 Standard ML入門』
SML#の開発者大堀先生が書かれた本。
『プログラミング言語ML』
むかし読んだが、わかりやすかったと思います。

F#

F#入門
わかりやすい入門サイト。会社のVisual StudioでがんばるならF#がいいかなと思って頑張り始めた。Haskellとかインスタンスするのに問題ないことの申請とか大変すぎるので。
F#
総本山
try F#
ブラウザで実行するF#チュートリアル
Midoliy |> F# - 型プロバイダ
TypeProviderがたのしそう
TypeProviderで生成したクラスをC#で使うための方法 | Moonmile Solutions Blog
C#ではTypeProviderがないから、、
F*: A Higher-Order Effectful Language Designed for Program Verification
依存型をもった言語らしい。Coqよりこっちのが自分の実用に近いのかな?F# + 依存型なのか?それともF#と無関係か?
F* Tutorial
上記のチュートリアル。Web処理系があるのがうれしい。
The Early History of the F# Languageの翻訳
翻訳で分かりづらいところもあるけど面白い。翻訳元The Early History of F# (HOPL IV - first draft)
C#/JavaScriptで学ぶF#入門 - Qiita
@7shiによる。なんだか得るものがあった気がする。
Sorting Excel rows alphabetically in F# (Office.Interop) - Stack Overflow
Excelをいじる、F#で

Lisp

Practical Scheme
プログラミング言語Schemeの紹介、海外エッセーの翻訳、「普通のやつらの上を行け」等。
Scheme手習い - The Little Schemer -
Let Over Lambda 50 Years of Lisp
LISPのマクロってすごいらしい。
『初めての人のためのLISP』
LISP入門の名著。復刊。
Gauche - A Scheme Implementation
プログラミング言語Schemeのスクリプト処理系である。R5RS準拠。多バイト文字列を組み込みでサポート。
JAKLD Javaアプリケーション組み込み用のLispドライバ
Javaで記述されたSchemeのインタープリタ。湯淺太一先生が作られたようです。
TUTScheme,TUTScheme/Tkの処理系
Lispの名言が凄すぎる
「私が知る中で、書く人がタイピングよりも考える事に費やす時間が長い言語は、SQL, Lisp, Haskellだけだ。 - Philip Greenspun」とあるが、タイピングが多いプログラマほど、肉体労働に近いわけだな、ふむふむ。
How to Design Programs
デザインレシピを使った設計方法の説明の本らしいです。電子ブック本文あり。読んでみたい。Lispを使って説明していあるらしいので、とりあえずここに分類。
マンガで分かるLisp(Manga Guide to Lisp)
ミクちゃんが説明してくれる!
魔法言語 リリカル☆Lisp
ノベルゲーム風のLispチュートリアル。すすんでるな。。。
Web系女子がLispと出会って統計学に目覚めるまでのお話
Schemeプログラマのレベル10

SICP

Structure and Interpretation of Computer Programs (MIT Electrical Engineering and Computer Science)
タイトルの頭文字をとってSICPとか、魔術師本と呼ばれてます。ソフトウェアの設計、構成法の本質を学ぶなら、この一冊かもしれない。表示の魔術師の絵がなんとも魅力的。プログラミング言語の説明本はたくさんあるけど、プログラムの部品の作り方、組み合わせてプログラム全体を構成する方法を説明した本は数少ない。この本がまずは決定版ではないだろうか。まだ私も7割がたしか読んでませんが、オススメです。
Welcome to the SICP Web Site (Structure and Interpretation of Computer Programs )
SICPのオンラインページ。この本は英語ならこのサイトで全文読めます。
『計算機プログラムの構造と解釈』
上記、日本語訳。日本語ページSICP Web Site for the Japanese Editionで、html版SICP、つまり、日本語訳全文が公開された!
ぺた語義:京大における Lisp を使ったプログラミング教育
京大でLISPを教えているのは、LISPプログラマを養成するためではないそうです。「プログラミングというのは、単に与えられた問題をコーディングする技術でなく、計算機科学の成果であるさまざまな概念や機能を駆使できる能力である。この意味で、講義で採用しているSICPは、きわめて適切な教科書である。」SICPでLISPの方言であるSchemeで解説しているので、LISPを使っているというわけです。本文では、「SICPは、これらを単に概念として紹介するのではなく、Lispでどのように実現されているかを具体的に解説している。」とあります。Lispってのは、シンプルにいろんなことを実現できるので、仕組みの説明にすごく向いていると思います。この記事は、プロ組ラング言語を理解してだけでは、プログラミングには不足なのだと言っている、いい記事ですね。計算機科学の成果をしっかり学ぶことが大事だという点、同感です。
CS 61A Home Page
University of California BerkeleyではSICPの内容をプログラミング言語をPythonに変えて教えてるみたいです。講義ノートもあります。
6.S184 - Zombies drink caffeinated 6.001
最近MITではSICPは講義から無くなってしまったようですが、Independent Activities Period(IAP)という短期間の講義でSICPの内容が教えられているそうです。参考:濃縮還元オレンジニュース:MITにてSICPのクラスが復活!?|gihyo.jp … 技術評論社
6.01 Homepage / Spring 2012
もともとSICPだった講義は内容も改められ、やはりプログラミング言語をPythonになっているようです。
本当のプログラミング初心者がSICPを読んではいけない三つの理由
いまSICPを読むのは時間の無駄
ほんとかなあ
本の虫: MITがSICPを教えなくなった理由
こちらはSICPの教師によるコメントだから説得力があるがSICPの価値はそれでも価値はあると思う。

プログラマ

『ハッカーと画家 コンピュータ時代の創造者たち』
プログラマの気骨を語っているエッセイ。おすすめです。
ぼくはこうしてプログラミングを覚えた
フェイスブックのエンジニアで史上ベスト3に入るといわれるEvan Priestley氏へのインタビュー。
歴史に残るハッカー10人
名前くらいは知っておきたい伝説のプログラマーたち - UEI shi3zの日記
プログラマの区分 Memoized Recursion
ファンタジーのキャラっぽく分類。おもしろい。
落ちこぼれだった私が、プログラマとして企業を越えて自由に生きる「夢を叶える方法」
fukamachiさんの方法と経緯。プログラムを書き続けたことがポイントな気がする。
Twitter 社採用面接受験記
一度は食べたい至高のプログラマー焼きとん 新宿ささもと - UEI shi3zの日記
60%の人間はプログラミングの素質がない

QuickCheck

QuickCheckでデータ駆動型テストを行う
QuickCheck - Wikipedia, the free encyclopedia
Haskell以外でも使えるようです。
QuickCheckも動かす:test-framework - nabeyangの日記
404 Blog Not Found:バカはバカにならない - 書評 - ファジング:ブルートフォースによる脆弱性発見手法
QuickCheckにも言及あります。

The Coq Proof Assistant

The Coq Proof Assistant
Coq本家。
Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions (Texts in Theoretical Computer Science. An EATCS Series)
coq artってやつですね。こいつが鉄板なんだろうか。積読です。
Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化
コンパクトなcoq入門すかね、日本語だと初のCoq本らしいっす。プログラム検証って感じではない。
Proof General
Emacs上のCoqフロントエンド。Generalの顔が怖い!
fm-forum @ ウィキ - Coq参考資料
名古屋大学の講義資料「数理解析・計算機数学 III」
下の方。
Asai Laboratory, Ochanomizu University
Coqゼミのコーナーがあります。
プログラミング Coq 絶対にバグのないプログラムの書き方
大学生によるCoqチュートリアル。
Coq クィックリファレンス
日本語のリファレンス。途中。
Software Foundations
TAPLのBenjamin C. Pierceさんの電子ブック。教科書らしい。このコースは以下のことをするとのこと。
「It develop basic concepts of functional programming, logic, operational semantics, lambda-calculus, and static type systems, using the Coq proof assistant.」
読んでみたい。

モデル検査

Spin - Formal Verification
ポピュラーなモデル検査器。
The SMV System
これまたポピュラーなモデルチェッカー。
LTSA - Labelled Transition System Analyser
CSPを先祖にもつFSP記法がまあまあシンプルで好きです。Spinよりさくっと美しく書ける。規模が大きいとなるとSpinのが実用的かも。アップデートがJune 2006で止まっているけど、まあまあ使えるレベルまでいったということかもしれません。
PAT: Process Analysis Toolkit
シンガポール発の、モデル検査ツール(シミュレーションとかもできる)。CSPの拡張(グローバル変数相当もサポート)していて、実用的にしているようで興味深い。他にも確率、リアルタイム性に関する検証ができるようだ。

形式手法

定理証明リンク集 - The curse of λ
Programming Language Foundations in Agda
The TLA Home Page
AWSにおける形式手法 - masateruk’s blogで知った。アマゾンさんがやってるって言うとすごいのかなとか思っちゃう。
B method
コード詳細化が特徴。いまでもコード詳細化って重要なのかが興味あるところ。
高信頼ソフトウェア構築技術に関する動向調査 調査報告書
パリ地下鉄14号線の信号システムが「Bメソッドを適用」、「これまでにバグがない」。

CSP

Communicating Sequential Processes (CSP)
ホーア(Tony Hoare)による、CSPの教科書の電子版(free)。
WoTUG
CSPの応用、普及しているフォーラム。
CSPコンソーシアム
日本のCSPの団体。存在を知らなかった。
PAT: Process Analysis Toolkit
シンガポール発の、モデル検査ツール(シミュレーションとかもできる)。CSPの拡張(グローバル変数相当もサポート)していて、実用的にしているようで興味深い。他にも確率、リアルタイム性に関する検証ができるようだ。

圏論

プログラマのための圏論の基礎(仮題)
圏論によるプログラミングと論理(灘校パソコン研究部 文化祭2013)
2013年 圏論勉強会 資料
スピヴァックの圏論教科書

ツール

NTEmacs JP
エディタ。カスタマイズ可能で、Coq-modeやHaskell mode等サポート。使ってます。ここを参考。gnu-packからインストールしてみた。カスタマイズはこのへんしてます。Emacsで「最近使ったファイル」 ウインドウを最大化したい。EmacsWiki: W Thirty Two Send Sys Command
color-theme homepage
Emacsのテーマがえ。色がえ。
codepad
オンラインのコンパイラ、インタープリタ。
Happy Hacking Keyboard Professional BT 日本語配列/墨 PD-KB620B
プロならキーボードもこだわろう。仕事で使っている。プライベートでもほしいところ。妻は許すだろうか。。静電容量で省スペース、打鍵感もよい。Bluetoothでゲーブルもない。和田英一先生の言葉です。
アメリカ西部のカウボーイたちは、馬が死ぬと馬はそこに残していくが、どんなに砂漠を歩こうとも、鞍は自分で担いで往く。馬は消耗品であり、鞍は自分の体に馴染んだインタフェースだからだ。いまやパソコンは消耗品であり、キーボードは大切な、生涯使えるインタフェースであることを忘れてはいけない。
Happy Hacking Keyboard | 和田先生関連ページ
Emacsを開発したリチャード・ストールマンも使っている。ノートPCの上におくスタイルは尊師スタイルと呼ばれているらしいwwwRichard Stallman and OLPC
社畜ちゃん台詞メーカー
Infer | A static analyzer for mobile apps | Infer
C言語、Objective-C、Javaの静的検証器。Facebookが買収しOSSになった。Infer Introduction - ::Eldesh a b = LEFT a | RIGHT b]

プログラミング関係のブログ

sumiiの日記
あどけない話
結城浩の日記
keigoiの日記
にわとり小屋でのプログラミング日記
檜山正幸のキマイラ飼育記

関数型言語使用の企業

Tsuru Capital
Haskellを使用する金融企業。
株式会社ぺあのしすてむ
F#とCoqを使用する。
株式会社時雨堂
Erlangを使用する。WebRTC に関する様々なソフトウェアを開発する。
F# ガイド | Microsoft Docs
MicrosoftはVisual StudioでF#をサポートする。

大学、研究室

小林研究室
東京大学 大学院情報理工学系研究科 コンピュータ科学専攻。高階モデル検査とか。
小林・住井研究室 東北大学
型システムなどの手法を利用したプログラム解析の研究
Jacques Garrigue : Home Page
Label-selective lambda-calculus and Transformation calculusなど
IIJ Innovation Institute [山本 和彦 主幹研究員]
Mewを作られた方。Haskellも書かれてます。

学会

ICFP (The International Conference on Functional Programming)
関数型言語の国際学会
International Symposium on Functional and Logic Programming
日本ソフトウェア科学会 プログラミング論研究会 (PPL)

プログラミングコンテスト

Top Coder
プログラマのメジャーリーグ。コンペティションに参加すると、レーティングされ、プログラミング能力を証明する。世界中から参加。
ICFP Programming Contest
国際的なプログラミングコンテスト?