Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic

Julian Biendarra 1 Jasmin Blanchette 2, 3, 4 Aymeric Bouzy 5 Martin Desharnais 6 Mathias Fleury 2, 3 Johannes Hölzl 7 Ondřej Kunčar 1 Andreas Lochbihler 8 Fabian Meier 9 Lorenz Panny 10 Andrei Popescu 11, 12 Christian Sternagel 13 René Thiemann 13 Dmitriy Traytel 8
1 TUM - Technische Universität München [München]
2 MPII - Max-Planck-Institut für Informatik
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
4 VU - Vrije Universiteit Amsterdam [Amsterdam]
5 InstantJob
6 LMU - Ludwig Maximilian University [Munich]
7 Computer Science Department - Carnegie Mellon University
8 ETH Zürich - Eidgenössische Technische Hochschule [Zürich]
9 Google Switzerland
10 TU/e - Technische Universiteit Eindhoven
11 IMAR - "Simion Stoilow" Institute of Mathematics
12 Middlesex University [London]
13 Department of Computer Science [Innsbruck]
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.
Type de document :
Communication dans un congrès
Clare Dixon and Marcelo Finger. Frontiers of Combining Systems, 11th International Symposium, Sep 2017, Brasilia, Brazil. Springer, 10483, pp.3-21, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-319-66167-4_1〉
Liste complète des métadonnées

Littérature citée [58 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01592196
Contributeur : Stephan Merz <>
Soumis le : mercredi 27 septembre 2017 - 15:12:59
Dernière modification le : jeudi 11 janvier 2018 - 06:23:13
Document(s) archivé(s) le : jeudi 28 décembre 2017 - 12:42:34

Fichier

BiendarraBlanchetteEtAl-FroCos...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

LORIA | LORIA-FM | UNIV-LORRAINE | INRIA2017 | INRIA

Citation

Julian Biendarra, Jasmin Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, et al.. Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. Clare Dixon and Marcelo Finger. Frontiers of Combining Systems, 11th International Symposium, Sep 2017, Brasilia, Brazil. Springer, 10483, pp.3-21, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-319-66167-4_1〉. 〈hal-01592196〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

306

Téléchargements de fichiers

20

Contact


archive-ouverte@inria.fr