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. red. / Gerwin Klein; Ruben Gamboa. Bind 8558 Springer, Cham, 2014. s. 93-110 (LNCS).
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Harvard
Blanchette, JC, Hölzl, J, Lochbihler, A, Panny, L, Popescu, A
& Traytel, D 2014,
Truly Modular (Co)datatypes for Isabelle/HOL. i G Klein & R Gamboa (red),
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. bind 8558, Springer, Cham, LNCS, s. 93-110.
https://doi.org/10.1007/978-3-319-08970-6_7APA
Blanchette, J. C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A.
, & Traytel, D. (2014).
Truly Modular (Co)datatypes for Isabelle/HOL. I G. Klein, & R. Gamboa (red.),
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 (Bind 8558, s. 93-110). Springer, Cham. LNCS
https://doi.org/10.1007/978-3-319-08970-6_7Vancouver
Blanchette JC, Hölzl J, Lochbihler A, Panny L, Popescu A
, Traytel D.
Truly Modular (Co)datatypes for Isabelle/HOL. I Klein G, Gamboa R, red., 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. Bind 8558. Springer, Cham. 2014. s. 93-110. (LNCS).
https://doi.org/10.1007/978-3-319-08970-6_7Author
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. red. / Gerwin Klein ; Ruben Gamboa. Bind 8558 Springer, Cham, 2014. s. 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 -
