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 language | English |
---|---|
Title of host publication | Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Proceedings |
Editors | C. Dixon, M. Finger |
Place of Publication | Dordrecht |
Publisher | Springer |
Pages | 3-21 |
Number of pages | 19 |
ISBN (Electronic) | 978-3-319-66167-4 |
ISBN (Print) | 978-3-319-66166-7 |
DOIs | |
Publication status | Published - 1 Jan 2017 |
Event | 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017) - Brasilia, Brazil Duration: 27 Sep 2017 → 29 Sep 2017 Conference number: 11 http://frocos2017.cic.unb.br |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 10483 LNAI |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017) |
---|---|
Abbreviated title | FroCoS 2017 |
Country/Territory | Brazil |
City | Brasilia |
Period | 27/09/17 → 29/09/17 |
Internet address |