Foundational (co)datatypes and (co)recursion for higher-order logic

Julian Biendarra; Jasmin Christian Blanchette; Aymeric Bouzy; Martin Desharnais; Mathias Fleury; Johannes Hölzl; Ondřej Kunčar; Andreas Lochbihler; Fabian Meier; Lorenz Panny; Andrei Popescu; Christian Sternagel; René Thiemann; Dmitriy Traytel

doi:10.1007/978-3-319-66167-4_1

Foundational (co)datatypes and (co)recursion for higher-order logic

Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondřej Kunčar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel

Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

14 Zitate (Scopus)

Abstract

We describe a line of work that started in 2011 towards enriching Isabelle/HOL’s language with coinductive datatypes, which allow infinite values, and with a more expressive notion of inductive datatype than previously supported by any system based on higher-order logic. These (co)datatypes are complemented by definitional principles for (co)recursive functions and reasoning principles for (co)induction. In contrast with other systems offering codatatypes, no additional axioms or logic extensions are necessary with our approach.

Originalsprache	Englisch
Titel	Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Proceedings
Redakteure/-innen	Clare Dixon, Marcelo Finger
Herausgeber (Verlag)	Springer Verlag
Seiten	3-21
Seitenumfang	19
ISBN (Print)	9783319661667
DOIs	https://doi.org/10.1007/978-3-319-66167-4_1
Publikationsstatus	Veröffentlicht - 2017
Extern publiziert	Ja
Veranstaltung	11th International Symposium on Frontiers of Combining Systems, FroCoS 2017 - Brasilia, Brasilien Dauer: 27 Sept. 2017 → 29 Sept. 2017

Publikationsreihe

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Band	10483 LNAI
ISSN (Print)	0302-9743
ISSN (elektronisch)	1611-3349

Konferenz

Konferenz	11th International Symposium on Frontiers of Combining Systems, FroCoS 2017
Land/Gebiet	Brasilien
Ort	Brasilia
Zeitraum	27/09/17 → 29/09/17

Zugriff auf Dokument

10.1007/978-3-319-66167-4_1

Andere Dateien und Links

Verknüpfung zur Publikation in Scopus

Dieses zitieren

Biendarra, J., Blanchette, J. C., Bouzy, A., Desharnais, M., Fleury, M., Hölzl, J., Kunčar, O., Lochbihler, A., Meier, F., Panny, L., Popescu, A., Sternagel, C., Thiemann, R., & Traytel, D. (2017). Foundational (co)datatypes and (co)recursion for higher-order logic. in C. Dixon, & M. Finger (Hrsg.), Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Proceedings (S. 3-21). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 10483 LNAI). Springer Verlag. https://doi.org/10.1007/978-3-319-66167-4_1

Biendarra, Julian ; Blanchette, Jasmin Christian ; Bouzy, Aymeric et al. / Foundational (co)datatypes and (co)recursion for higher-order logic. Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Proceedings. Hrsg. / Clare Dixon ; Marcelo Finger. Springer Verlag, 2017. S. 3-21 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{35132568e99b4d18af85b560dbd20b3a,

title = "Foundational (co)datatypes and (co)recursion for higher-order logic",

abstract = "We describe a line of work that started in 2011 towards enriching Isabelle/HOL{\textquoteright}s language with coinductive datatypes, which allow infinite values, and with a more expressive notion of inductive datatype than previously supported by any system based on higher-order logic. These (co)datatypes are complemented by definitional principles for (co)recursive functions and reasoning principles for (co)induction. In contrast with other systems offering codatatypes, no additional axioms or logic extensions are necessary with our approach.",

author = "Julian Biendarra and Blanchette, {Jasmin Christian} and Aymeric Bouzy and Martin Desharnais and Mathias Fleury and Johannes H{\"o}lzl and Ond{\v r}ej Kun{\v c}ar and Andreas Lochbihler and Fabian Meier and Lorenz Panny and Andrei Popescu and Christian Sternagel and Ren{\'e} Thiemann and Dmitriy Traytel",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2017.; 11th International Symposium on Frontiers of Combining Systems, FroCoS 2017 ; Conference date: 27-09-2017 Through 29-09-2017",

year = "2017",

doi = "10.1007/978-3-319-66167-4_1",

language = "English",

isbn = "9783319661667",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "3--21",

editor = "Clare Dixon and Marcelo Finger",

booktitle = "Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Proceedings",

}

Biendarra, J, Blanchette, JC, Bouzy, A, Desharnais, M, Fleury, M, Hölzl, J, Kunčar, O, Lochbihler, A, Meier, F, Panny, L, Popescu, A, Sternagel, C, Thiemann, R & Traytel, D 2017, Foundational (co)datatypes and (co)recursion for higher-order logic. in C Dixon & M Finger (Hrsg.), Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bd. 10483 LNAI, Springer Verlag, S. 3-21, 11th International Symposium on Frontiers of Combining Systems, FroCoS 2017, Brasilia, Brasilien, 27/09/17. https://doi.org/10.1007/978-3-319-66167-4_1

Foundational (co)datatypes and (co)recursion for higher-order logic. / Biendarra, Julian; Blanchette, Jasmin Christian; Bouzy, Aymeric et al.
Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Proceedings. Hrsg. / Clare Dixon; Marcelo Finger. Springer Verlag, 2017. S. 3-21 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 10483 LNAI).

Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

TY - GEN

T1 - Foundational (co)datatypes and (co)recursion for higher-order logic

AU - Biendarra, Julian

AU - Blanchette, Jasmin Christian

AU - Bouzy, Aymeric

AU - Desharnais, Martin

AU - Fleury, Mathias

AU - Hölzl, Johannes

AU - Kunčar, Ondřej

AU - Lochbihler, Andreas

AU - Meier, Fabian

AU - Panny, Lorenz

AU - Popescu, Andrei

AU - Sternagel, Christian

AU - Thiemann, René

AU - Traytel, Dmitriy

PY - 2017

Y1 - 2017

N2 - We describe a line of work that started in 2011 towards enriching Isabelle/HOL’s language with coinductive datatypes, which allow infinite values, and with a more expressive notion of inductive datatype than previously supported by any system based on higher-order logic. These (co)datatypes are complemented by definitional principles for (co)recursive functions and reasoning principles for (co)induction. In contrast with other systems offering codatatypes, no additional axioms or logic extensions are necessary with our approach.

AB - We describe a line of work that started in 2011 towards enriching Isabelle/HOL’s language with coinductive datatypes, which allow infinite values, and with a more expressive notion of inductive datatype than previously supported by any system based on higher-order logic. These (co)datatypes are complemented by definitional principles for (co)recursive functions and reasoning principles for (co)induction. In contrast with other systems offering codatatypes, no additional axioms or logic extensions are necessary with our approach.

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

U2 - 10.1007/978-3-319-66167-4_1

DO - 10.1007/978-3-319-66167-4_1

M3 - Conference contribution

AN - SCOPUS:85029586986

SN - 9783319661667

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 3

EP - 21

BT - Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Proceedings

A2 - Dixon, Clare

A2 - Finger, Marcelo

PB - Springer Verlag

T2 - 11th International Symposium on Frontiers of Combining Systems, FroCoS 2017

Y2 - 27 September 2017 through 29 September 2017

ER -

Biendarra J, Blanchette JC, Bouzy A, Desharnais M, Fleury M, Hölzl J et al. Foundational (co)datatypes and (co)recursion for higher-order logic. in Dixon C, Finger M, Hrsg., Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Proceedings. Springer Verlag. 2017. S. 3-21. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-66167-4_1

Foundational (co)datatypes and (co)recursion for higher-order logic

Abstract

Publikationsreihe

Konferenz

Zugriff auf Dokument

Andere Dateien und Links

Fingerprint

Dieses zitieren