Truly Modular (Co)datatypes for Isabelle/HOL

Jasmin Christian Blanchette; Johannes Hölzl; Andreas Lochbihler; Lorenz Panny; Andrei Popescu; Dmitriy Traytel

doi:10.1007/978-3-319-08970-6_7

Truly Modular (Co)datatypes for Isabelle/HOL

Jasmin Christian Blanchette
, Johannes Hölzl
, Andreas Lochbihler
, Lorenz Panny
, Andrei Popescu
, Dmitriy Traytel

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

Originele taal-2	Engels
Titel	Interactive Theorem Proving
Subtitel	5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings
Redacteuren	Gerwin Klein, Ruben Gamboa
Uitgeverij	Springer
Pagina's	93-110
ISBN van elektronische versie	978-3-319-08970-6
ISBN van geprinte versie	978-3-319-08969-0
DOI's	https://doi.org/10.1007/978-3-319-08970-6_7
Status	Gepubliceerd - 2014
Extern gepubliceerd	Ja

Publicatie series

Naam	Lecture Notes in Computer Science
Volume	8558

Toegang tot document

10.1007/978-3-319-08970-6_7

Citeer dit

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 (editors), Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings (blz. 93-110). (Lecture Notes in Computer Science; Vol. 8558). Springer. https://doi.org/10.1007/978-3-319-08970-6_7

Blanchette, Jasmin Christian ; Hölzl, Johannes ; Lochbihler, Andreas et al. / Truly Modular (Co)datatypes for Isabelle/HOL. Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings. redacteur / Gerwin Klein ; Ruben Gamboa. Springer, 2014. blz. 93-110 (Lecture Notes in Computer Science).

@inproceedings{64c8e667ef1b4f8384e2c94e0733f51b,

title = "Truly Modular (Co)datatypes for Isabelle/HOL",

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",

isbn = "978-3-319-08969-0",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "93--110",

editor = "Gerwin Klein and Ruben Gamboa",

booktitle = "Interactive Theorem Proving",

address = "Germany",

}

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 (reds.), Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings. Lecture Notes in Computer Science, vol. 8558, Springer, blz. 93-110. https://doi.org/10.1007/978-3-319-08970-6_7

Truly Modular (Co)datatypes for Isabelle/HOL. / Blanchette, Jasmin Christian; Hölzl, Johannes; Lochbihler, Andreas et al.
Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings. reds. / Gerwin Klein; Ruben Gamboa. Springer, 2014. blz. 93-110 (Lecture Notes in Computer Science; Vol. 8558).

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

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

U2 - 10.1007/978-3-319-08970-6_7

DO - 10.1007/978-3-319-08970-6_7

M3 - Conference contribution

SN - 978-3-319-08969-0

T3 - Lecture Notes in Computer Science

SP - 93

EP - 110

BT - Interactive Theorem Proving

A2 - Klein, Gerwin

A2 - Gamboa, Ruben

PB - Springer

ER -

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, redacteurs, Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings. Springer. 2014. blz. 93-110. (Lecture Notes in Computer Science). doi: 10.1007/978-3-319-08970-6_7