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

*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

23 Downloads (Pure)

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 languageEnglish
Title of host publicationFrontiers of Combining Systems
Subtitle of host publication11th International Symposium, FroCoS 2017, Brasília, Brazil, September 27-29, 2017, Proceedings
EditorsClare Dixon, Marcelo Finger
PublisherSpringer/Verlag
Pages3-21
Number of pages19
ISBN (Electronic)9783319661674
ISBN (Print)9783319661667
DOIs
Publication statusPublished - 2017
Event11th International Symposium on Frontiers of Combining Systems, FroCoS 2017 - Brasilia, Brazil
Duration: 27 Sept 201729 Sept 2017

Publication series

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

Conference

Conference11th International Symposium on Frontiers of Combining Systems, FroCoS 2017
Country/TerritoryBrazil
CityBrasilia
Period27/09/1729/09/17

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.

FundersFunder number
European Union’s Horizon 2020 research and innovation programNI 491/10-2, NI 491/13-2, NI 491/13-3, NI 491/15-1
Horizon 2020 Framework Programme713999, 643161
Engineering and Physical Sciences Research CouncilEP/N019547/1
European Research Council
Deutsche ForschungsgemeinschaftNI 491/11-2, NI 491/14-1
Schweizerischer Nationalfonds zur Förderung der Wissenschaftlichen Forschung153217
Austrian Science FundY757, P27502

    Fingerprint

    Dive into the research topics of 'Foundational (co)datatypes and (co)recursion for higher-order logic'. Together they form a unique fingerprint.

    Cite this