TY - GEN
T1 - Truly modular (Co)datatypes for Isabelle/HOL
AU - Blanchette, Jasmin Christian
AU - Hölzl, Johannes
AU - Lochbihler, Andreas
AU - Panny, Lorenz
AU - Popescu, Andrei
AU - Traytel, Dmitriy
PY - 2014
Y1 - 2014
N2 - We extended Isabelle/HOL with a pair of definitional commands for datatypes and codatatypes. They support mutual and nested (co)recursion through well-behaved type constructors, including mixed recursion-corecursion, and are complemented by syntaxes for introducing primitively (co)recursive functions and by a general proof method for reasoning coinductively. As a case study, we ported Isabelle's Coinductive library to use the new commands, eliminating the need for tedious ad hoc constructions.
AB - We extended Isabelle/HOL with a pair of definitional commands for datatypes and codatatypes. They support mutual and nested (co)recursion through well-behaved type constructors, including mixed recursion-corecursion, and are complemented by syntaxes for introducing primitively (co)recursive functions and by a general proof method for reasoning coinductively. As a case study, we ported Isabelle's Coinductive library to use the new commands, eliminating the need for tedious ad hoc constructions.
UR - http://www.scopus.com/inward/record.url?scp=84904796220&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-08970-6_7
DO - 10.1007/978-3-319-08970-6_7
M3 - Conference contribution
AN - SCOPUS:84904796220
SN - 9783319089690
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 93
EP - 110
BT - Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
PB - Springer Verlag
T2 - 5th International Conference on Interactive Theorem Proving, ITP 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014
Y2 - 14 July 2014 through 17 July 2014
ER -