Copenhagen Programming Language Seminar

Inductive Reasoning about Effectful Data Types

Kristian StÝvring
University of Aarhus / FIRST

Thursday, September 27, 14:30-15:00 (!)
DIKU, Universitetsparken 1, Room N018


We present a pair of reasoning principles, <em>definition</em> and <em>proof</em> by <em>rigid induction<//em>, which can be seen as proper generalizations of lazy-datatype induction to monadic effects other than partiality. We further show how these principles can be integrated into logical-relations arguments, and obtain as a particular instance a general and principled proof that the success-stream and failure-continuation models of backtracking are equivalent. As another application, we present a monadic model of general search trees, not necessarily traversed depth-first. The results are applicable to both lazy and eager languages, and we emphasize this by presenting most examples in both Haskell and SML.

Joint work with Andrzej Filinski. (This is a preview of an ICFP'07 presentation, so not all aspects mentioned above will be covered to any significant extent.)

Scientific host: Andrzej Filinski . Administrative host: Annette Enggaard . All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org