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

Julian Biendarra; Jasmin 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 Blanchette ^{2, 3, 4} Aymeric Bouzy ⁵ Martin Desharnais ⁶ Mathias Fleury ^{2, 3} Johannes Hölzl ⁷ Ondřej Kunčar ¹ Andreas Lochbihler ⁸ Fabian Meier ⁹ Lorenz Panny ¹⁰ Andrei Popescu ^{11, 12} Christian Sternagel ¹³ René Thiemann ¹³ Dmitriy Traytel ⁸

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

LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik

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 - Swiss Federal Institute of Technology in Zürich [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.

Document type :

Conference papers

Domain :

Computer Science [cs] / Logic in Computer Science [cs.LO]

Complete list of metadatas

Cited literature [54 references] Display Hide Download

https://hal.inria.fr/hal-01592196
Contributor : Stephan Merz <>
Submitted on : Wednesday, September 27, 2017 - 3:12:59 PM
Last modification on : Thursday, August 22, 2019 - 12:10:38 PM
Long-term archiving on: Thursday, December 28, 2017 - 12:42:34 PM

BiendarraBlanchetteEtAl-FroCos...

Files produced by the author(s)

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

File

Identifiers

Collections

Citation

Export

Metrics

650

158

Contact

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

File

Identifiers

Collections

Citation

Export

Share

Metrics

650

158

Contact