本研究では、構成的型理論の上でワールドとワールドマップを利用するプログラミングの有効性を、圏論的定式化と、命令型言語との能力の比較という2つの側面から研究した。圏論的定式化では、まず既存研究をAgda言語によって形式化した。その結果、既存研究では曖昧であった圏とE-圏の区別を明確にし、ワールドとワールドマップがなすのは圏ではなくE-圏であることを示した。そして、ワールドマップのE-圏Wを構成するために必須の公理の証明を新たに記した。さらに、E-圏WにおいてE-終対象、E-積を構成した。命令型言語との能力の比較では、構成的型理論の上でワールドを利用するプログラミングが命令型言語に相当する表現力を持つことを示した。具体的には、基本的な命令を持つ命令型プログラミング言語の構文と意味を定義し、その言語のワールドの枠組みによる解釈を構成した。そして、その解釈が元のプログラムの意味を保つことを証明した。
本発表では、まずワールドとワールドマップによるプログラミングを概説し、その上で研究成果を述べる。