Inductive Reasoning About Effectful Data Types

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

We present a pair of reasoning principles, definition and proof by rigid induction, 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.
Original languageEnglish
Title of host publicationICFP 07 : Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming, Freiburg, Germany, October 1-3, 2007
PublisherAssociation for Computing Machinery
Publication date2007
Pages97-110
ISBN (Print)978-1-59593-815-2
DOIs
Publication statusPublished - 2007
EventACM/SIGPLAN International Conference on Functional Programming - Freiburg, Germany
Duration: 1 Oct 20073 Oct 2007
Conference number: 12

Conference

ConferenceACM/SIGPLAN International Conference on Functional Programming
Nummer12
LandGermany
ByFreiburg
Periode01/10/200703/10/2007
SeriesSIGPLAN Notices
Number42 (9)
ISSN0362-1340

ID: 1050059