についてはPOPL 2004で何か言っていたような気もします。ちゃんと聞いていなかったので何も覚えていませんし（←駄目）、既出かもしれませんが。
あと、一般的な再帰型があれば一般的な不動点演算子が型付けできるし、ボトムにも（任意の）型を与えられるので、当然の結果として論理の体系としては不健全になるかと。＞元の方
POPL 2004といえば、自分はbisimulationやらlogical relationやらの研究をしている（つもりの）わけですが、rとlが上手に発音できないので、発表のたびに苦労します。
追記：激しく被った。（「被った」のところにリンクがあります。って、スタイルシートを修正しろよ！＞自分）
