Standard
Fast Verified BCD Subtyping. / Bessai, Jan; Rehof, Jakob; Düdder, Boris.
Models, Mindsets, Meta: The What, the How, and the Why Not?. ed. / Tiziana Margaria; Susann Graf; Kim G. Larsen. Springer, 2019. p. 356-371 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 11200 LNCS).
Research output: Chapter in Book/Report/Conference proceeding › Book chapter › Research › peer-review
Harvard
Bessai, J, Rehof, J
& Düdder, B 2019,
Fast Verified BCD Subtyping. in T Margaria, S Graf & KG Larsen (eds),
Models, Mindsets, Meta: The What, the How, and the Why Not?. Springer, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11200 LNCS, pp. 356-371.
https://doi.org/10.1007/978-3-030-22348-9_21APA
Bessai, J., Rehof, J.
, & Düdder, B. (2019).
Fast Verified BCD Subtyping. In T. Margaria, S. Graf, & K. G. Larsen (Eds.),
Models, Mindsets, Meta: The What, the How, and the Why Not? (pp. 356-371). Springer. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 11200 LNCS
https://doi.org/10.1007/978-3-030-22348-9_21Vancouver
Bessai J, Rehof J
, Düdder B.
Fast Verified BCD Subtyping. In Margaria T, Graf S, Larsen KG, editors, Models, Mindsets, Meta: The What, the How, and the Why Not?. Springer. 2019. p. 356-371. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 11200 LNCS).
https://doi.org/10.1007/978-3-030-22348-9_21Author
Bessai, Jan ; Rehof, Jakob ; Düdder, Boris. / Fast Verified BCD Subtyping. Models, Mindsets, Meta: The What, the How, and the Why Not?. editor / Tiziana Margaria ; Susann Graf ; Kim G. Larsen. Springer, 2019. pp. 356-371 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 11200 LNCS).
Bibtex
@inbook{31729ecb4e104def900c9b7fe5a8fb0c,
title = "Fast Verified BCD Subtyping",
abstract = "A decision procedure for the Barendregt-Coppo-Dezani subtype relation on intersection types (“BCD subtyping”) is presented and formally verified in Coq. Types are extended with unary, covariant, distributing, preordered type constructors and binary products. A quadratic upper bound on the algorithm runtime is established. The formalization can be compiled to executable OCaml or Haskell code using the extraction mechanism of Coq.",
keywords = "BCD, Coq, Intersection types, Subtyping",
author = "Jan Bessai and Jakob Rehof and Boris D{\"u}dder",
year = "2019",
month = jan,
day = "1",
doi = "10.1007/978-3-030-22348-9_21",
language = "English",
isbn = "978-3-030-22347-2",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "356--371",
editor = "Tiziana Margaria and Susann Graf and Larsen, {Kim G.}",
booktitle = "Models, Mindsets, Meta",
address = "Switzerland",
}
RIS
TY - CHAP
T1 - Fast Verified BCD Subtyping
AU - Bessai, Jan
AU - Rehof, Jakob
AU - Düdder, Boris
PY - 2019/1/1
Y1 - 2019/1/1
N2 - A decision procedure for the Barendregt-Coppo-Dezani subtype relation on intersection types (“BCD subtyping”) is presented and formally verified in Coq. Types are extended with unary, covariant, distributing, preordered type constructors and binary products. A quadratic upper bound on the algorithm runtime is established. The formalization can be compiled to executable OCaml or Haskell code using the extraction mechanism of Coq.
AB - A decision procedure for the Barendregt-Coppo-Dezani subtype relation on intersection types (“BCD subtyping”) is presented and formally verified in Coq. Types are extended with unary, covariant, distributing, preordered type constructors and binary products. A quadratic upper bound on the algorithm runtime is established. The formalization can be compiled to executable OCaml or Haskell code using the extraction mechanism of Coq.
KW - BCD
KW - Coq
KW - Intersection types
KW - Subtyping
UR - http://www.scopus.com/inward/record.url?scp=85068012056&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-22348-9_21
DO - 10.1007/978-3-030-22348-9_21
M3 - Book chapter
AN - SCOPUS:85068012056
SN - 978-3-030-22347-2
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 356
EP - 371
BT - Models, Mindsets, Meta
A2 - Margaria, Tiziana
A2 - Graf, Susann
A2 - Larsen, Kim G.
PB - Springer
ER -
