第22回大会ポスターデモセッション概要

[PD-1]  証明支援系Agda  
AgdaはChalmers工科大学(スウェーデン)において開発 中の対話型証明支援系ソフトである。Agda はMartin- Loef 型理論を基礎とし、表現されたプログラムを実行す る機能と、表現された論理の正しい推論を支援する機能 とを併せ持っている。本デモでは、Agdaの使用例を二つ 取り上げる。一つは代数系に関する証明で多用される等 号の取り扱いであり、もう一つは、様相mu 計算を用いた あるwhile programの安全性証明である。
 
[PD-2]  グリッド環境上で動作する並列制約解消システム  
グリッド計算環境上で動作する並列制約解消システムg-HECSを紹介する.本 システムの目的は,スケジューリング・資源配置などの制約充足問題,最適 化問題を高速に解くことである.g-HECSではグリッド計算環境上で複数異種 の制約ソルバが協調的に並列動作し,解探索を行う.ユーザはフロントエン ドとして表計算ソフトOpenOffice.org Calcを利用でき,シート上で問題の記 述,解探索,得られた解の2次加工が容易に行える.
 
[PD-3]  スプレッドシートと様々なシステムをつなぐオープンミドルウェアの設計  
スプレッドシートと様々なシステムを接続するのオープンミドルウェア について発表する.本ミドルウェアの目的は,スプレッドシートという リッチなGUIを種々のシステムのフロントエンドとして容易に組み込む ことを可能にすることである.本発表では,提案ミドルウェアの応用例 として,スプレッドシート上でセルに式を記述することで制約プログラミング を行うことができるシステムである制約スプレッドシートのデモを行う.
 
[PD-4]  System Support for Software Updates on Virtual Private Servers  
We are developing a virtual private server (VPS) system based on the SoftwarePot secure execution system. Our system makes it possible to share files and directories between VPSes by path mapping. The existing SoftwarePot has two problems with regard to software updates. First, files are shared in a read-only manner, so updating shared files is not possible. Second, SoftwarePot does not support testing a new version while the previous version is running. We propose two extensions to SoftwarePot that address these problems. The first extension is update mode that makes updating of shared files possible. Modifications to shared files are saved as private files and remapped automatically. The second extension is test mode that allows testing of a new version of a VPS while the previous version is running. In test mode, a replica of the original VPS is created and run with a substitute IP address. Experimental results show that our system can reduce disk usage by 36% to 93% while maintaining the capability to modify any file. Runtime overhead in update mode increased by 1% when compared to normal mode.
 
[PD-5]  Haskellによるスキーマ推論プログラム  
XML文書からその文書を扱うHaskell APIを自動生成するプロ グラムを構築する際には,まずXML文書からXMLの適切なスキー マを推論する機能を実装することが必要である.本発表ではこの機能を Haskellで実装したのでその概要について報告する.具体的には、DTD, RelaxNG, XMLSchemaで表現されるスキーマの推論をJavaで実装したTrangの ロジックを用いて実装している.
 
[PD-6]  Eclipseの内部構造とHaskell開発環境  
現在Eclipse上に実装されているHaskell向けの統合開発環境を検討し、 改良すべき点を挙げ、そしてこれらの改善のため現在開発中の環境について説明を する。 Eclipseを使うにあたって、HaskellプログラマとHaskellを知らないプログラマでは 求められる機能が異なると考えられるがここでは主に後者に重点を置いてHaskell プログラミングを始める際の障壁を低くする事を目標とする。
 
[PD-7]  Open induction in Isabelle/HOL  
一般に帰納法はWell-founded な順序構造に基づいているが、Well-founded でない 順序構造においてopenな性質を対象にした open induction がRaoult により 1988年に提案されている(Information Processing Letter, Vol.29, pp.19-23)。 本発表では、Isabelle/HOL における open induction のライブラリおよびそれを用いた Higman の補題の証明(Geser, 1996)のIsabelle/HOLにおける試みについて述べる。
 
[PD-8]  ビジュアル言語Viscuit  
ビジュアル言語Viscuitはビットマップで表現された図形の組で現された書換規則 からなる言語である。その実行は、図形上のクリックイベントで起動され、 図形の位置・傾きなどからもっとも近いと判断された書換規則の左辺とマッチング して右辺に置き換える。本デモでは、計算機の専門家ではないイラストレータなど によりViscuit で作られた動く絵本などを紹介し、さらにViscuit Land の構想を 紹介する。
 
[PD-9]  独創的な三次元アプリケーションを開発するためのAPIの設計と実装  
我々はLG3D上で斬新な3Dアプリケーションを開発するために,3Dアプリケーションを 作るための便利なAPI(CosmoAPI)を設計した.CosmoAPIは開発者が思い描く独創的な インターフェースを容易に実現することを目的として設計した.我々はCosmoAPIを 用いて「Cosmo Scheduler D」を開発し,JavaOneにて高評価を得た.本論文では, このCosmoAPIを紹介し,LG3DのAPIを直接使うよりも便利であることを示す.
 
[PD-10]  デジタル万華鏡  
画像圧縮の分野で知られているフラクタル画像圧縮(FIC)は画像内の自己相似性に 注目し, 幾何学的な解析を自動的に行う. FICによる画像解析の結果として, 画像は それをなすアフィン変換の集合に置き換えられる. このアフィン変換群を復号する 際に, 画像中のピクセルは整数列からなる反復関数系アドレスを持つ. この反復関数系 アドレスを別の画像に関連付け, ある画像からある画像へ色彩を転送し, 芸術的な 変換効果を得ることができる. この手法によって, ユーザは単に2種類の画像を 用意するだけで芸術的な効果を得ることができる.
 
[PD-11]  UMLのクラス図における論理プログラミングを用いた無矛盾検査  
クラス属性、多重度、汎化関係、排他関係を許すUMLクラス図において、 UMLクラス図を論理プログラムに変換して矛盾チェックする手法を提案し、 クラス図が矛盾していれば、その箇所を図上で表示を行うプロトタイプ システムのデモを行う。