Copenhagen Programming Language Seminar
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 email@example.com with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org