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

Filinski, A & Støvring, K 2007, Inductive Reasoning About Effectful Data Types. in ICFP 07: Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming, Freiburg, Germany, October 1-3, 2007. Association for Computing Machinery, SIGPLAN Notices, no. 42 (9), pp. 97-110, ACM/SIGPLAN International Conference on Functional Programming, Freiburg, Germany, 01/10/2007. https://doi.org/10.1145/1291151.1291168

APA

Filinski, A., & Støvring, K. (2007). Inductive Reasoning About Effectful Data Types. In ICFP 07: Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming, Freiburg, Germany, October 1-3, 2007 (pp. 97-110). Association for Computing Machinery. SIGPLAN Notices No. 42 (9) https://doi.org/10.1145/1291151.1291168

Vancouver

Filinski A, Støvring K. Inductive Reasoning About Effectful Data Types. In 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)). https://doi.org/10.1145/1291151.1291168

Author

Filinski, Andrzej ; Støvring, Kristian. / Inductive Reasoning About Effectful Data Types. ICFP 07: Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming, Freiburg, Germany, October 1-3, 2007. Association for Computing Machinery, 2007. pp. 97-110 (SIGPLAN Notices; No. 42 (9)).

Bibtex

@inproceedings{4f609d5065b511dcbee902004c4f4f50,
title = "Inductive Reasoning About Effectful Data Types",
abstract = "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.",
author = "Andrzej Filinski and Kristian St{\o}vring",
year = "2007",
doi = "10.1145/1291151.1291168",
language = "English",
isbn = "978-1-59593-815-2",
series = "SIGPLAN Notices",
publisher = "Association for Computing Machinery",
number = "42 (9)",
pages = "97--110",
booktitle = "ICFP 07",
note = "null ; Conference date: 01-10-2007 Through 03-10-2007",

}

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