Back to Search
Start Over
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
- Source :
- Frontiers of Combining Systems, 11th International Symposium, Frontiers of Combining Systems, 11th International Symposium, Sep 2017, Brasilia, Brazil. pp.3-21, ⟨10.1007/978-3-319-66167-4_1⟩, Frontiers of Combining Systems-11th International Symposium, FroCoS 2017, Proceedings, 3-21, STARTPAGE=3;ENDPAGE=21;TITLE=Frontiers of Combining Systems-11th International Symposium, FroCoS 2017, Proceedings, 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 . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10483 LNAI, Springer/Verlag, 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, Lecture Notes in Computer Science, Lecture Notes in Computer Science-Frontiers of Combining Systems, 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017), Frontiers of Combining Systems ISBN: 9783319661667, FroCoS, Frontiers of Combining Systems
- Publication Year :
- 2017
- Publisher :
- Zenodo, 2017.
-
Abstract
- International audience; 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.
- Subjects :
- Recursion
Programming language
Coinduction
HOL
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
020207 software engineering
0102 computer and information sciences
02 engineering and technology
computer.software_genre
01 natural sciences
Higher-order logic
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
010201 computation theory & mathematics
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Line (geometry)
0202 electrical engineering, electronic engineering, information engineering
Recursive functions
computer
Axiom
Mathematics
Subjects
Details
- ISBN :
- 978-3-319-66166-7
978-3-319-66167-4 - ISSN :
- 03029743 and 16113349
- ISBNs :
- 9783319661667 and 9783319661674
- Database :
- OpenAIRE
- Journal :
- Frontiers of Combining Systems, 11th International Symposium, Frontiers of Combining Systems, 11th International Symposium, Sep 2017, Brasilia, Brazil. pp.3-21, ⟨10.1007/978-3-319-66167-4_1⟩, Frontiers of Combining Systems-11th International Symposium, FroCoS 2017, Proceedings, 3-21, STARTPAGE=3;ENDPAGE=21;TITLE=Frontiers of Combining Systems-11th International Symposium, FroCoS 2017, Proceedings, 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 . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10483 LNAI, Springer/Verlag, 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, Lecture Notes in Computer Science, Lecture Notes in Computer Science-Frontiers of Combining Systems, 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017), Frontiers of Combining Systems ISBN: 9783319661667, FroCoS, Frontiers of Combining Systems
- Accession number :
- edsair.doi.dedup.....be47e57f3a4668a0d42d7a1834212db4
- Full Text :
- https://doi.org/10.5281/zenodo.3228084