Lambda the Ultimate

inactiveTopic A Modal Language for Effects
started 4/23/2004; 2:48:33 AM - last post 4/23/2004; 2:48:33 AM
Ehud Lamm - A Modal Language for Effects  blueArrow
4/23/2004; 2:48:33 AM (reads: 9788, responses: 0)
A Modal Language for Effects
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