We present a typed A-calculus which enables us to handle
first-class environments. The syntax and the reduction are obtained by
applying the idea of Curien's "explicit substitution". The type system
has ML-polymorphism and a type inference algorithm which is sound
and terminates.
各種検索
サポート
ヘルプ