概要

〇XML文書変換の正しさの検証
インターネットの世界では、ある仕様に従うXML文書から別の仕様に従うXML文書への変換が頻繁に行われます。そのような変換を記述する言語としてXSLTが有名です。しかし、XSLTで記述された変換プログラムは、仕様に関係なく変換を行うので、仕様を満たさないXML文書を生成してしまう場合があります。また、仕様は満たしていても望ましくない文書を生成したり、変換そのものが停止しないこともあります。
変換プログラムがこのようなことを起こさない、つまりプログラムが行う変換が「正しい」ことを、変換を行う前に検証できるようなXML文書変換言語を設計しています。

〇理論に基づいた言語設計
変換プログラムの正しさを保証するためには、変換の振る舞いを解析するための理論が必要になります。
ここでは、「型理論」と「項書き換え系」と呼ばれる理論をベースとして、その理論を構築し、それに基づいて言語を設計しています。また、理論に基づいて言語を設計することで、変換の正しさを保証しつつ、従来の変換言語では記述しづらいような強力な変換方法を提案することができるようになります。

講座・グループ

研究カテゴリー

活動分野
ソフトウェア
関連キーワード