Standard
Truly Modular (Co)datatypes for Isabelle/HOL. / Blanchette, Jasmin Christian; Hölzl, Johannes; Lochbihler, Andreas; Panny, Lorenz; Popescu, Andrei; Traytel, Dmitriy.
ITP 2014 - : 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings. ed. / Gerwin Klein; Ruben Gamboa. Vol. 8558 Springer, Cham, 2014. p. 93-110 (LNCS).
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
Blanchette, JC, Hölzl, J, Lochbihler, A, Panny, L, Popescu, A
& Traytel, D 2014,
Truly Modular (Co)datatypes for Isabelle/HOL. in G Klein & R Gamboa (eds),
ITP 2014 - : 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings. vol. 8558, Springer, Cham, LNCS, pp. 93-110.
https://doi.org/10.1007/978-3-319-08970-6_7
APA
Blanchette, J. C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A.
, & Traytel, D. (2014).
Truly Modular (Co)datatypes for Isabelle/HOL. In G. Klein, & R. Gamboa (Eds.),
ITP 2014 - : 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings (Vol. 8558, pp. 93-110). Springer, Cham. LNCS
https://doi.org/10.1007/978-3-319-08970-6_7
Vancouver
Blanchette JC, Hölzl J, Lochbihler A, Panny L, Popescu A
, Traytel D.
Truly Modular (Co)datatypes for Isabelle/HOL. In Klein G, Gamboa R, editors, ITP 2014 - : 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings. Vol. 8558. Springer, Cham. 2014. p. 93-110. (LNCS).
https://doi.org/10.1007/978-3-319-08970-6_7
Author
Blanchette, Jasmin Christian ; Hölzl, Johannes ; Lochbihler, Andreas ; Panny, Lorenz ; Popescu, Andrei ; Traytel, Dmitriy. / Truly Modular (Co)datatypes for Isabelle/HOL. ITP 2014 - : 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings. editor / Gerwin Klein ; Ruben Gamboa. Vol. 8558 Springer, Cham, 2014. pp. 93-110 (LNCS).
Bibtex
@inproceedings{d359a1da1ef7422dad52bf0fda116794,
title = "Truly Modular (Co)datatypes for Isabelle/HOL",
abstract = "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{\textquoteright}s Coinductive library to use the new commands, eliminating the need for tedious ad hoc constructions.",
author = "Blanchette, {Jasmin Christian} and Johannes H{\"o}lzl and Andreas Lochbihler and Lorenz Panny and Andrei Popescu and Dmitriy Traytel",
year = "2014",
doi = "10.1007/978-3-319-08970-6_7",
language = "English",
volume = "8558",
series = "LNCS",
pages = "93--110",
editor = "Gerwin Klein and Ruben Gamboa",
booktitle = "ITP 2014 -",
publisher = "Springer, Cham",
}
RIS
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.
U2 - 10.1007/978-3-319-08970-6_7
DO - 10.1007/978-3-319-08970-6_7
M3 - Article in proceedings
VL - 8558
T3 - LNCS
SP - 93
EP - 110
BT - ITP 2014 -
A2 - Klein, Gerwin
A2 - Gamboa, Ruben
PB - Springer, Cham
ER -