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

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

15 Citations (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.

Original language	English
Title of host publication	Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Proceedings
Editors	C. Dixon, M. Finger
Place of Publication	Dordrecht
Publisher	Springer
Pages	3-21
Number of pages	19
ISBN (Electronic)	978-3-319-66167-4
ISBN (Print)	978-3-319-66166-7
DOIs	https://doi.org/10.1007/978-3-319-66167-4_1
Publication status	Published - 1 Jan 2017
Event	11th International Symposium on Frontiers of Combining Systems (FroCoS 2017) - Brasilia, Brazil Duration: 27 Sept 2017 → 29 Sept 2017 Conference number: 11 http://frocos2017.cic.unb.br

Publication series

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

Conference

Conference	11th International Symposium on Frontiers of Combining Systems (FroCoS 2017)
Abbreviated title	FroCoS 2017
Country/Territory	Brazil
City	Brasilia
Period	27/09/17 → 29/09/17
Internet address	http://frocos2017.cic.unb.br

Funding

Blanchette was supported by the Deutsche Forschungsgemeinschaft (DFG) projects “Quis Custodiet” (NI 491/11-2) and “Den Hammer härten” (NI 491/14-1). He also received funding from the European Research Council under the European Union’s Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Hölzl was supported by the DFG project “Verifikation probabilistischer Modelle in interaktiven Theorembeweisern” (NI 491/15-1). Kunˇcar and Popescu were supported by the DFG project “Security Type Systems and Deduction” (NI 491/13-2 and NI 491/13-3) as part of the program Reliably Secure Software Systems (RS3, priority program 1496). Kunˇcar was also supported by the DFG project “Integration der Logik HOL mit den Programmiersprachen ML und Haskell” (NI 491/10-2). Lochbihler was supported by the Swiss National Science Foundation (SNSF) grant “Formalising Computational Soundness for Protocol Implementations” (153217). Popescu was supported by the UK Engineering and Physical Sciences Research Council (EPSRC) starting grant “VOWS: Verification of Web-based Systems” (EP/N019547/1). Sternagel and Thiemann were supported by the Austrian Science Fund (FWF): P27502 and Y757. Traytel was supported by the DFG program “Programm-und Modell-Analyse” (PUMA, doctorate program 1480). The authors are listed alphabetically.

Access to Document

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

Cite this

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 (Eds.), Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Proceedings (pp. 3-21). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10483 LNAI). Springer. 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. editor / C. Dixon ; M. Finger. Dordrecht : Springer, 2017. pp. 3-21 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{f87ff6be321441a49d4118d3bc1029f7,

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",

year = "2017",

month = jan,

day = "1",

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

language = "English",

isbn = "978-3-319-66166-7",

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

publisher = "Springer",

pages = "3--21",

editor = "C. Dixon and M. Finger",

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

address = "Germany",

note = "11th International Symposium on Frontiers of Combining Systems (FroCoS 2017), FroCoS 2017 ; Conference date: 27-09-2017 Through 29-09-2017",

url = "http://frocos2017.cic.unb.br",

}

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 (eds), 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), vol. 10483 LNAI, Springer, Dordrecht, pp. 3-21, 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017), Brasilia, Brazil, 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. ed. / C. Dixon; M. Finger. Dordrecht: Springer, 2017. p. 3-21 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10483 LNAI).

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

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

N1 - Conference code: 11

PY - 2017/1/1

Y1 - 2017/1/1

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 - https://www.scopus.com/pages/publications/85029586986

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 - 978-3-319-66166-7

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, C.

A2 - Finger, M.

PB - Springer

CY - Dordrecht

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, editors, Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Proceedings. Dordrecht: Springer. 2017. p. 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

Publication series

Conference

Funding

Access to Document

Other files and links

Fingerprint

Cite this