Fibrational induction meets effects

Robert Atkey, Neil Ghani, Bart Jacobs, Patricia Johann

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

10 Citations (Scopus)

Abstract

This paper provides several induction rules that can be used to prove properties of effectful data types. Our results are semantic in nature and build upon Hermida and Jacobs’ fibrational formulation of induction for polynomial data types and its extension to all inductive data types by Ghani, Johann, and Fumex. An effectful data type μ(TF) is built from a functor F that describes data, and a monad T that computes effects. Our main contribution is to derive induction rules that are generic over all functors F and monads T such that μ(TF) exists. Along the way, we also derive a principle of definition by structural recursion for effectful data types that is similarly generic. Our induction rule is also generic over the kinds of properties to be proved: like the work on which we build, we work in a general fibrational setting and so can accommodate very general notions of properties, rather than just those of particular syntactic forms. We give examples exploiting the generality of our results, and show how our results specialize to those in the literature, particularly those of Filinski and Støvring.
LanguageEnglish
Title of host publicationFoundations of Software Science and Computational Structures
Subtitle of host publication15th International Conference, FOSSACS 2011
EditorsLars Birkedal
PublisherSpringer
Pages42-57
Number of pages16
Volume7213
DOIs
Publication statusPublished - 2012
Event15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012 - Tallinn, Estonia
Duration: 24 Mar 20121 Apr 2012

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume7213
ISSN (Print)0302-9743

Conference

Conference15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012
Abbreviated titleFOSSACS 2012
CountryEstonia
CityTallinn
Period24/03/121/04/12

Fingerprint

Syntactics
Semantics
Polynomials

Keywords

  • fibrational induction
  • polynomial data types

Cite this

Atkey, R., Ghani, N., Jacobs, B., & Johann, P. (2012). Fibrational induction meets effects. In L. Birkedal (Ed.), Foundations of Software Science and Computational Structures: 15th International Conference, FOSSACS 2011 (Vol. 7213, pp. 42-57). (Lecture Notes in Computer Science; Vol. 7213). Springer. https://doi.org/10.1007/978-3-642-28729-9_3
Atkey, Robert ; Ghani, Neil ; Jacobs, Bart ; Johann, Patricia. / Fibrational induction meets effects. Foundations of Software Science and Computational Structures: 15th International Conference, FOSSACS 2011. editor / Lars Birkedal. Vol. 7213 Springer, 2012. pp. 42-57 (Lecture Notes in Computer Science).
@inproceedings{48766d81c9124e95ada9ddd5f940ea77,
title = "Fibrational induction meets effects",
abstract = "This paper provides several induction rules that can be used to prove properties of effectful data types. Our results are semantic in nature and build upon Hermida and Jacobs’ fibrational formulation of induction for polynomial data types and its extension to all inductive data types by Ghani, Johann, and Fumex. An effectful data type μ(TF) is built from a functor F that describes data, and a monad T that computes effects. Our main contribution is to derive induction rules that are generic over all functors F and monads T such that μ(TF) exists. Along the way, we also derive a principle of definition by structural recursion for effectful data types that is similarly generic. Our induction rule is also generic over the kinds of properties to be proved: like the work on which we build, we work in a general fibrational setting and so can accommodate very general notions of properties, rather than just those of particular syntactic forms. We give examples exploiting the generality of our results, and show how our results specialize to those in the literature, particularly those of Filinski and St{\o}vring.",
keywords = "fibrational induction, polynomial data types",
author = "Robert Atkey and Neil Ghani and Bart Jacobs and Patricia Johann",
year = "2012",
doi = "10.1007/978-3-642-28729-9_3",
language = "English",
volume = "7213",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "42--57",
editor = "Lars Birkedal",
booktitle = "Foundations of Software Science and Computational Structures",

}

Atkey, R, Ghani, N, Jacobs, B & Johann, P 2012, Fibrational induction meets effects. in L Birkedal (ed.), Foundations of Software Science and Computational Structures: 15th International Conference, FOSSACS 2011. vol. 7213, Lecture Notes in Computer Science, vol. 7213, Springer, pp. 42-57, 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, 24/03/12. https://doi.org/10.1007/978-3-642-28729-9_3

Fibrational induction meets effects. / Atkey, Robert; Ghani, Neil; Jacobs, Bart; Johann, Patricia.

Foundations of Software Science and Computational Structures: 15th International Conference, FOSSACS 2011. ed. / Lars Birkedal. Vol. 7213 Springer, 2012. p. 42-57 (Lecture Notes in Computer Science; Vol. 7213).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

TY - GEN

T1 - Fibrational induction meets effects

AU - Atkey, Robert

AU - Ghani, Neil

AU - Jacobs, Bart

AU - Johann, Patricia

PY - 2012

Y1 - 2012

N2 - This paper provides several induction rules that can be used to prove properties of effectful data types. Our results are semantic in nature and build upon Hermida and Jacobs’ fibrational formulation of induction for polynomial data types and its extension to all inductive data types by Ghani, Johann, and Fumex. An effectful data type μ(TF) is built from a functor F that describes data, and a monad T that computes effects. Our main contribution is to derive induction rules that are generic over all functors F and monads T such that μ(TF) exists. Along the way, we also derive a principle of definition by structural recursion for effectful data types that is similarly generic. Our induction rule is also generic over the kinds of properties to be proved: like the work on which we build, we work in a general fibrational setting and so can accommodate very general notions of properties, rather than just those of particular syntactic forms. We give examples exploiting the generality of our results, and show how our results specialize to those in the literature, particularly those of Filinski and Støvring.

AB - This paper provides several induction rules that can be used to prove properties of effectful data types. Our results are semantic in nature and build upon Hermida and Jacobs’ fibrational formulation of induction for polynomial data types and its extension to all inductive data types by Ghani, Johann, and Fumex. An effectful data type μ(TF) is built from a functor F that describes data, and a monad T that computes effects. Our main contribution is to derive induction rules that are generic over all functors F and monads T such that μ(TF) exists. Along the way, we also derive a principle of definition by structural recursion for effectful data types that is similarly generic. Our induction rule is also generic over the kinds of properties to be proved: like the work on which we build, we work in a general fibrational setting and so can accommodate very general notions of properties, rather than just those of particular syntactic forms. We give examples exploiting the generality of our results, and show how our results specialize to those in the literature, particularly those of Filinski and Støvring.

KW - fibrational induction

KW - polynomial data types

UR - http://www.scopus.com/inward/record.url?scp=84859129534&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-28729-9_3

DO - 10.1007/978-3-642-28729-9_3

M3 - Conference contribution book

VL - 7213

T3 - Lecture Notes in Computer Science

SP - 42

EP - 57

BT - Foundations of Software Science and Computational Structures

A2 - Birkedal, Lars

PB - Springer

ER -

Atkey R, Ghani N, Jacobs B, Johann P. Fibrational induction meets effects. In Birkedal L, editor, Foundations of Software Science and Computational Structures: 15th International Conference, FOSSACS 2011. Vol. 7213. Springer. 2012. p. 42-57. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-28729-9_3