PCES PI Meeting     Feb 2001
25
Expression Types
•�A — terms denoting expressions of type A
•Introduction rule (constructor)
•D ; • |- E : A
•          D ; G |- box E : �A
•E depends only on expression variables!