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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Original language	English
Title of host publication	Interactive Theorem Proving
Subtitle of host publication	5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings
Editors	Gerwin Klein, Ruben Gamboa
Publisher	Springer
Pages	93-110
ISBN (Electronic)	978-3-319-08970-6
ISBN (Print)	978-3-319-08969-0
DOIs	https://doi.org/10.1007/978-3-319-08970-6_7
Publication status	Published - 2014
Externally published	Yes

Publication series

Name	Lecture Notes in Computer Science
Volume	8558

Access to Document

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

Cite this

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.), 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 (pp. 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. editor / Gerwin Klein ; Ruben Gamboa. Springer, 2014. pp. 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 (eds), 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, pp. 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. ed. / Gerwin Klein; Ruben Gamboa. Springer, 2014. p. 93-110 (Lecture Notes in Computer Science; Vol. 8558).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › 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, 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. Springer. 2014. p. 93-110. (Lecture Notes in Computer Science). doi: 10.1007/978-3-319-08970-6_7