[Colloquium] Show & Tell Series at TTI-C (2/22/05 @ 12:15pm)

Katherine Cumming kcumming at tti-c.org
Mon Feb 14 16:27:08 CST 2005


TTI-C SHOW AND TELL SERIES TALK
 
Speaker: Derek Dreyer, TTI-C
Speaker's home page: http://www.tti-c.org//dreyer.html
 
Time: Tuesday, February 22nd
Location: TTI-C Conference Room
Lunch/Refreshments Provided  @ 12:00pm 
Seminar @ 12:15pm
 
Title: The Safe Recursion Problem
Abstract:
Recursive modules are one of the most commonly requested extensions to
ML. A basic question that arises in the design of a recursive module
extension is how to deal with the interaction of recursion and
computational effects. In particular, it is useful to allow recursive
modules to invoke arbitrary effectful code at initialization time, but
then it is necessary for safety purposes to ensure that recursive
identifiers are not used prematurely (i.e. before initialization is
finished). I call this the "safe recursion" problem.

In this talk, I will describe a type system that I developed for
statically ensuring safe recursion at the level of the simply typed
lambda-calculus. The basic idea is to track the use of a recursive
identifier as if it were an effectful operation, and to only permit
recursive definitions if they are "pure" with respect to this kind of
effect. This kind of effect is rather unusual, though, in that at some
point it "loses its potency" and can thereafter be safely ignored.
Another idea, relevant to supporting separate compilation of recursive
modules, is to distinguish the notions of "referencing" and
"dereferencing" a recursive identifier.

I will explain how my approach improves on existing proposals for
ensuring safe recursion. I will also consider some important practical
concerns, including: separate compilation of recursive modules, type
inference, and incorporating my type system into ML. No prior knowledge
of ML is necessary, only some basic familiarity with the
lambda-calculus. 
 
-----------------
If you have questions, or would like to meet the speaker, please contact
Katherine at 4-1994 or kcumming at tti-c.org.  For information on future
TTI-C talks or events, please go to the TTI-C Events page:
http://www.tti-c.org/events.html
 
 
 
 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20050214/9306ce48/attachment.htm


More information about the Colloquium mailing list