次々回: 1992年 5月 21日 (木) 電通大 (予定)
葉書の残りは 枚です
差出人(幹事):
113 文京区本郷 7-3-1
東京大学工学部計数工学科 岩崎英哉
03-3812-2111 ext. 7411
iwasaki@wadalab.t.u-tokyo.ac.jp
型理論の依存型の概念を説明し、依存型によってプログラム・モジュール の記述を行なう方法を説明した。また、その考えに基づいて設計している仕様 記述／プログラミング言語Ｍａｙａによる仕様記述およびプログラムの例を紹 介した。
おまけ 質問の時に、この方面の入門書をきかれましたが、その時詳しい
reference を出せなかったので、ここで紹介しておきます。
まず、
@book{NPS90,
author={{Bengt Nordstr\"{o}m, Kent Petersson and Jan M.\ Smith}},
title={Programming in Martin-L\"{o}f's Type Theory, An Introduction},
publisher={Oxford University Press},
city={Oxford},
year=1990}
は Martin-L\"{o}f の型理論を使うための入門書です。
Martin-L\"{o}f の型理論といっても実はいろいろバージョンがある
のですが、この本は、それらの関係をある程度あきらかにしてくれま
す。
また、
@book{Thompson91,
author="Simon Thompson",
title={Type theory and functional programming},
publisher={Addison-Wesley},
year=1991}
も応用のための入門書ですが、特に関数型プログラミングへの応用に
ついて、NPS90 よりもいろいろな話題を取り扱っています。
Martin-L\"{o}f の型理論とはちょっと毛色が違う別の系統のものと
して、型付きλ計算を拡張した体系がいろいろあります。次の論文は
それを見とおしよくまとめたものです。
@article{Barendregt91,
author="H.P.\ Barendregt",
title={Introduction to generalised type systems},
journal={Journal of Functional Programming},
volume="1",
number="2",
pages="124-154",
year=1991}
また、コンピュータ・ソフトウェアの連載
@article{Tatsuta91-1,
author="龍田真",
title={型理論I},
journal={コンピュータソフトウェア},
volume="8",
number="1",
pages="25--33",
year=1991}
@article{Tatsuta91-2,
author="龍田真",
title={型理論II},
journal={コンピュータソフトウェア},
volume="8",
number="2",
pages="40--46",
year=1991}
@article{Tatsuta91-3,
author="龍田真",
title={型理論III},
journal={コンピュータソフトウェア},
volume="8",
number="3",
pages="2--8"
year=1991}
@article{Tatsuta91-4,
author="龍田真",
title={型理論IV},
journal={コンピュータソフトウェア},
volume="8",
number="4",
pages="56--68",
year=1991}
は日本語によるサーベイです。型理論そのものの紹介で、関数型プロ
グラミングとの関係についてはあまり扱われていませんが、
Martin-Lo\"{o}f の系統とgeneralized type system の系統の（こち
らはλcube という、ちょっと制限された形ですが）両方を扱ってい
ます。
最新の話題を知るための一つの方法に各種メイリングリストに加入す
ることがあります。Types mailing list は型理論のためのもので、
Fj のニュースにも fj.mail-list.types ニュースグループとして流
されています。また、sonoteno mailing list は主に日本国内のもの
で、「その手の」ことの話題を流すためのものです。どの手のという
のはぜんぜん決まっていませんが、型理論、論理学、圏論などの計算
機科学への応用に興味を持つ人がはいっているようです。以下に、こ
れらのメイリングリスト加入の連絡先を記します。Types の方は外国
ですから、当然ながら英語で書かないと通じません :-)。
Types types-request@theory.lcs.mit.edu
（これは Fj のニュースになっているから
それを見ることができれば、そっちの方が
便利）
Sonoteno sonoteno-request@sfc.keio.ac.jp
木下 佳樹 記
- --
KINOSHITA Yoshiki [KINOSHITA is my family name]
Computer Language Section, Computer Science Division
Electrotechnical Laboratory, 1-1-4 Umezono, Tsukuba, Ibaraki 305 Japan