[Colloquium] Reminder—-Nan evski talk today at 2:30

[Meridel Trimble]

Date: Friday, April 18th, 2003

Time: 2:30 p.m.

Place: Ryerson Hall 251 

Speaker: Aleksandar Nanevski
Carnegie Mellon University

http://www-2.cs.cmu.edu/afs/cs.cmu.edu/user/aleks/www/ 

Title: A modal foundation for functional programming with effects

Abstract: 
One of the most intriguing questions in the area of functional programming has 
always been how to safely combine pure functional programs with various 
imperative features like input/output or memory reads/writes. This combination 
is important because it improves the practicality, expressiveness and 
efficiency of functional programs while retaining the advantages that programs 
are easy to reason about and that their safety can be statically guaranteed. 

The most popular approach currently is to introduce effect analysis into type-
checking via monads. In a monadic system (such as that of Haskell) effects are 
confined to expressions with monadic type. However, monads also globalize the 
scope of the encapsulated effect: once an effect occurs, the purity of the 
surrounding computation cannot be restored. As a consequence, monadic typing 
does not provide good support for effects that could be handled (such as 
exceptions). 

In this talk I will present a way to remedy this deficiency, based on the 
observation of Pfenning and Davies that an abstract monad can be decomposed in 
terms of operators for possibility Diamond and necessity Box of modal logic. My 
idea is to use the Box modality (which is a co-monad) for tracking the 
propagation of effects, and leave the globalization of effect scope to Diamond. 
Then the effects that admit a natural notion of handling can be encoded using 
Box; since they are not global, there is no need to push them under Diamond. 
Using this idea, I develop a general framework for effect handling systems, and 
obtain novel calculi for exceptions, catch-and-throw, composable continuations, 
dynamic 

*Refreshments will be served after the talk in Ryerson 255* 

If you wish to meet with the speaker, please send e-mail to Meridel Trimble 
mtrimble at uchicago.edu