Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic - Archive ouverte HAL Access content directly
Conference Papers Year : 2017

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

(1) , (2, 3, 4) , (5) , (6) , (2, 3) , (7) , (1) , (8) , (9) , (10) , (11, 12) , (13) , (13) , (8)
1
2
3
4
5
6
7
8
9
10
11
12
13
Aymeric Bouzy
  • Function : Author
Fabian Meier
  • Function : Author

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.
Fichier principal
Vignette du fichier
BiendarraBlanchetteEtAl-FroCos.pdf (188.24 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01592196 , version 1 (27-09-2017)

Identifiers

Cite

Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, et al.. Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. Frontiers of Combining Systems, 11th International Symposium, Sep 2017, Brasilia, Brazil. pp.3-21, ⟨10.1007/978-3-319-66167-4_1⟩. ⟨hal-01592196⟩
536 View
140 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More