Foundational nonuniform (Co)datatypes for higher-order logic

Jasmin Christian Blanchette; Fabian Meier; Andrei Popescu; Dmitriy Traytel

doi:10.1109/LICS.2017.8005071

Foundational nonuniform (Co)datatypes for higher-order logic

Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

11 Downloads (Pure)

Abstract

Nonuniform (or 'nested' or 'heterogeneous') datatypes are recursively defined types in which the type arguments vary recursively. They arise in the implementation of finger trees and other efficient functional data structures. We show how to reduce a large class of nonuniform datatypes and codatatypes to uniform types in higher-order logic. We programmed this reduction in the Isabelle/HOL proof assistant, thereby enriching its specification language. Moreover, we derive (co)induction and (co)recursion principles based on a weak variant of parametricity.

Original language	English
Title of host publication	2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Subtitle of host publication	[Proceedings]
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	1-12
Number of pages	12
ISBN (Electronic)	9781509030187
ISBN (Print)	9781509030194
DOIs	https://doi.org/10.1109/LICS.2017.8005071
Publication status	Published - 2017
Event	32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017 - Reykjavik, Iceland Duration: 20 Jun 2017 → 23 Jun 2017

Conference

Conference	32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017
Country/Territory	Iceland
City	Reykjavik
Period	20/06/17 → 23/06/17

Funding

Acknowledgment: We thank David Basin for supporting this research, Peter Lammich for pointing us to his work on finger trees and for formalizing Okasaki’s construction for powerlists, Johannes Hölzl for taking the time to explain Lean’s nonuniform datatypes, and Mark Summerfield and the anonymous reviewers for suggesting textual improvements. Blanchette has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Popescu has received funding from UK’s Engineering and Physical Sciences Research Council (EPSRC) via the grant EP/N019547/1, Verification of Web Services (VOWS). The authors are listed alphabetically.

Funders	Funder number
EPSRC
European Research Council
European Union’s Horizon 2020
Horizon 2020 Framework Programme	713999
Engineering and Physical Sciences Research Council	EP/N019547/1

Access to Document

10.1109/LICS.2017.8005071

Foundational_nonuniform_Codatatypes_for_higher-order_logicFinal published version, 299 KBLicence: Article 25fa Dutch Copyright Act

Persistent URL (handle)

Persistent link

Cite this

@inproceedings{287c5b7b965e4da8af0ea105b9335876,

title = "Foundational nonuniform (Co)datatypes for higher-order logic",

abstract = "Nonuniform (or 'nested' or 'heterogeneous') datatypes are recursively defined types in which the type arguments vary recursively. They arise in the implementation of finger trees and other efficient functional data structures. We show how to reduce a large class of nonuniform datatypes and codatatypes to uniform types in higher-order logic. We programmed this reduction in the Isabelle/HOL proof assistant, thereby enriching its specification language. Moreover, we derive (co)induction and (co)recursion principles based on a weak variant of parametricity.",

author = "Blanchette, {Jasmin Christian} and Fabian Meier and Andrei Popescu and Dmitriy Traytel",

year = "2017",

doi = "10.1109/LICS.2017.8005071",

language = "English",

isbn = "9781509030194",

pages = "1--12",

booktitle = "2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

address = "United States",

note = "32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017 ; Conference date: 20-06-2017 Through 23-06-2017",

}

Blanchette, JC, Meier, F, Popescu, A & Traytel, D 2017, Foundational nonuniform (Co)datatypes for higher-order logic. in 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS): [Proceedings]., 8005071, Institute of Electrical and Electronics Engineers Inc., pp. 1-12, 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, 20/06/17. https://doi.org/10.1109/LICS.2017.8005071

Foundational nonuniform (Co)datatypes for higher-order logic. / Blanchette, Jasmin Christian; Meier, Fabian; Popescu, Andrei et al.
2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS): [Proceedings]. Institute of Electrical and Electronics Engineers Inc., 2017. p. 1-12 8005071.

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Foundational nonuniform (Co)datatypes for higher-order logic

AU - Blanchette, Jasmin Christian

AU - Meier, Fabian

AU - Popescu, Andrei

AU - Traytel, Dmitriy

PY - 2017

Y1 - 2017

N2 - Nonuniform (or 'nested' or 'heterogeneous') datatypes are recursively defined types in which the type arguments vary recursively. They arise in the implementation of finger trees and other efficient functional data structures. We show how to reduce a large class of nonuniform datatypes and codatatypes to uniform types in higher-order logic. We programmed this reduction in the Isabelle/HOL proof assistant, thereby enriching its specification language. Moreover, we derive (co)induction and (co)recursion principles based on a weak variant of parametricity.

AB - Nonuniform (or 'nested' or 'heterogeneous') datatypes are recursively defined types in which the type arguments vary recursively. They arise in the implementation of finger trees and other efficient functional data structures. We show how to reduce a large class of nonuniform datatypes and codatatypes to uniform types in higher-order logic. We programmed this reduction in the Isabelle/HOL proof assistant, thereby enriching its specification language. Moreover, we derive (co)induction and (co)recursion principles based on a weak variant of parametricity.

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

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

U2 - 10.1109/LICS.2017.8005071

DO - 10.1109/LICS.2017.8005071

M3 - Conference contribution

AN - SCOPUS:85029600863

SN - 9781509030194

SP - 1

EP - 12

BT - 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017

Y2 - 20 June 2017 through 23 June 2017

ER -

Foundational nonuniform (Co)datatypes for higher-order logic

Abstract

Conference

Funding

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this