Inductive Reasoning About Effectful Data Types

Andrzej Filinski; Kristian Støvring

doi:10.1145/1291151.1291168

Inductive Reasoning About Effectful Data Types

Andrzej Filinski, Kristian Støvring

Department of Computer Science

14 Citations (Scopus)

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.

Original language	English
Title of host publication	ICFP 07 : Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming, Freiburg, Germany, October 1-3, 2007
Publisher	Association for Computing Machinery
Publication date	2007
Pages	97-110
ISBN (Print)	978-1-59593-815-2
DOIs	https://doi.org/10.1145/1291151.1291168
Publication status	Published - 2007
Event	ACM/SIGPLAN International Conference on Functional Programming - Freiburg, Germany Duration: 1 Oct 2007 → 3 Oct 2007 Conference number: 12

Conference

Conference	ACM/SIGPLAN International Conference on Functional Programming
Number	12
Country/Territory	Germany
City	Freiburg
Period	01/10/2007 → 03/10/2007

Series	SIGPLAN Notices
Number	42 (9)
ISSN	0362-1340

Access to Document

10.1145/1291151.1291168

Cite this

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

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

@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 = "ACM/SIGPLAN International Conference on Functional Programming ; Conference date: 01-10-2007 Through 03-10-2007",

}

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

T2 - ACM/SIGPLAN International Conference on Functional Programming

Y2 - 1 October 2007 through 3 October 2007

ER -