イベントレポート:「Coqチュートリアル#1」
去る1月12日、定理証明支援系ツールCoqの初心者向けチュートリアルが開催さ れた(http://kokucheese.com/event/index/23667/)。今後も2月2日 (http://kokucheese.com/event/index/23744/)、2月9日、2月16日と引き続き開 催されていく予定である。本記事では、開催の様子をレポートする。
去る1月12日、定理証明支援系ツールCoqの初心者向けチュートリアルが開催さ れた(http://kokucheese.com/event/index/23667/)。今後も2月2日 (http://kokucheese.com/event/index/23744/)、2月9日、2月16日と引き続き開 催されていく予定である。本記事では、開催の様子をレポートする。
Go が初のメジャーリリースに到達した。Google では今回のリリースを今後数年間の安定バージョンと位置付けている。YouTube ではコアインフラストラクチャに Go を採用している。
今週初め、Ceylon IDEの最初のマイルストーンがリリースされた。これは、昨年の12月に初めてリリースされたプログラミング言語Ceylon用のIDEである。
Dartエディタのプレビルドバージョンが手に入るようになった。これはEclipseのDart IDEでDartを簡単に始められる。FrogはDartをJavascriptに変換するコンパイラだ。Dartで書かれていて、JythonとIronPythonの作者が実装している。また、DartチームはDart言語の説明を盛んに行い、nullable型のような型システムに関する機能の提案を行っている。
COMプログラミングは生きており、Windowsプラットフォーム上では健在だ、C++の新しい変形版は、COMプログラミングをもっと扱い易くしている。 C++ Component Extensions(C++コンポーネント拡張)として知られている、この新言語は、新しいWindowsランタイム、WinRTを作るために使われた。
ThoughtWorks は先日,テクノロジレーダ(Technology Radar) という報告書を発行した。技術的リーダたちが最新技術を理解して戦略的プラットフォームやツールを選定し,自らの組織の準備をするための資料だ。
![]()
GoogleはVMをともなう新しい言語であり、JSコンパイラでもあるDartをプレビューした。 InfoQはDartのアプリの構築に貢献する文法の裏側を探った:スナップショット、Isolate、モジュール方式
本記事ではCSPベースの「マルチドメイン・モデル検査ツール」である、PAT(Process Analysis Toolkit)について紹介する。モデル検査は、形式手法(Formal Method)という方法論を基礎とする技術であり、複雑さが増大しながらも安全性を求められる、現在のソフトウェア開発の状況に対する処方箋の1つとして注目されている手法である。
Alloyは、MITにて開発された仕様記述言語であり、ツールによる自動解析を使い、インクリメンタルに形式仕様が書けることが特長である。筆者らはAlloy開発者による、Alloyを使った形式手法入門書を翻訳、今夏にオーム社より刊行した。本記事では、Alloyの簡単な概要と、翻訳書『抽象によるソフトウェア設計』(「Alloy本」)を紹介する。
2011年9月25日「ProofSummit2011」が開催された。本イベントでは、形式手法の一種である定理証明支援系ツールに興味を持つ技術者が集まり、Coq,Agda等のツールのチュートリアル、および応用に関する講演が行われた。

オブジェクト指向と関数型の機能をすべて提供し、さらにRubyに代表される動的言語の柔軟性と静的型付け言語の信頼性をも兼ね備え、JavaVMの上で開発実行できる新時代の言語がScalaだ。Scalaとその上で使える強力なWebフレームワークLiftを用いた実システム開発が世界的に広がっているが、今回は日本での実システム開発の事例とScala採用の理由をインタビュー+プレゼン形式で語ってもらう。
GroovyServは、筆者が所属しているNTTソフトウェア株式会社において、Apache License, Version 2.0に基づき開発・公開しているオープンソースソフトウェアです。現在、Mac OS X、Linux、Windows版で動作確認を行い、これらの環境用のバイナリ版も公開しています 本記事ではGroovyServを紹介します。GroovyServの基本的なアイデアの説明に始まり、実際の効果を示した上で、導入方法と簡単な使い方、応用例などについても説明します。最後に、適用条件と制約について言及します。