Inductive Reasoning About Effectful Data Types
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Standard
Inductive Reasoning About Effectful Data Types. / Filinski, Andrzej; Støvring, Kristian.
ICFP 07: Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming, Freiburg, Germany, October 1-3, 2007. Association for Computing Machinery, 2007. p. 97-110 (SIGPLAN Notices; No. 42 (9)).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - Inductive Reasoning About Effectful Data Types
AU - Filinski, Andrzej
AU - Støvring, Kristian
N1 - Conference code: 12
PY - 2007
Y1 - 2007
N2 - 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.
AB - 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.
U2 - 10.1145/1291151.1291168
DO - 10.1145/1291151.1291168
M3 - Article in proceedings
SN - 978-1-59593-815-2
T3 - SIGPLAN Notices
SP - 97
EP - 110
BT - ICFP 07
PB - Association for Computing Machinery
Y2 - 1 October 2007 through 3 October 2007
ER -
ID: 1050059