あるAnonymous Coward 曰く、

産業技術総合研究所により、関数型プログラミング言語「Agda」の研修コースが開催されるそうです（産総研：システム検証研究センター：CVS研修コース「Agdaによる仕様記述」）。

Agdaは強力な依存型を備えた関数型プログラミング言語であり、証明支援システムとして利用できることでも知られています。また、その形式手法はプログラムの不具合を防ぐ開発手段として近年注目を集めています。

受講対象はAgdaに興味がある技術者、マネージャ、学生ということで、ある程度の開発経験があれば問題ないそうです。形式手法やバグのないプログラム開発に興味のあるみなさんも参加してみてはいかがでしょうか。