|
Sungwoo Park and Robert Harper.
Building on a judgmental formulation of lax logic, we propose a modal language
which can be used as a framework for practical programming languages with
effects. Its characteristic feature is a syntactic distinction between terms
and expressions, where terms denote values and expressions denote computations.
We distinguish between control effects and world effects, and allow control
effects only in terms and world effects only in expressions. Therefore the
distinction between values and computations is made only with respect to world
effects. We give an explanation of the type system and the operational
semantics from a modal logic perspective. We also introduce a term construct
similar to Haskell's runST construct and augment the type system to
ensure its safety.
Modal logic techniques are beoming more and more important. I suggest follwing the references to Pfenning's papers for further enlightenment.
Posted to theory by Ehud Lamm on 4/23/04; 2:49:16 AM
|
A Modal Language for Effects
