Fast Verified BCD Subtyping

Jan Bessai; Jakob Rehof; Boris Düdder

doi:10.1007/978-3-030-22348-9_21

Fast Verified BCD Subtyping

Jan Bessai^*, Jakob Rehof, Boris Düdder

^*Corresponding author af dette arbejde

2 Citationer (Scopus)

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.

Originalsprog	Engelsk
Titel	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Antal sider	16
Forlag	Springer Verlag
Publikationsdato	1 jan. 2019
Sider	356-371
DOI	https://doi.org/10.1007/978-3-030-22348-9_21
Status	Udgivet - 1 jan. 2019

Navn	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind	11200 LNCS
ISSN	0302-9743

Adgang til dokumentet

10.1007/978-3-030-22348-9_21

Andre filer og links

Link to publication in Scopus

Citationsformater

Bessai, J., Rehof, J., & Düdder, B. (2019). Fast Verified BCD Subtyping. I Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (s. 356-371). Springer Verlag. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Bind 11200 LNCS https://doi.org/10.1007/978-3-030-22348-9_21

Fast Verified BCD Subtyping. / Bessai, Jan; Rehof, Jakob; Düdder, Boris.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag, 2019. s. 356-371 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 11200 LNCS).

Publikation: Bidrag til bog/antologi/rapport › Bidrag til bog/antologi › Forskning › peer review

Bessai, J, Rehof, J & Düdder, B 2019, Fast Verified BCD Subtyping. i Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), bind 11200 LNCS, s. 356-371. https://doi.org/10.1007/978-3-030-22348-9_21

Bessai J, Rehof J, Düdder B. Fast Verified BCD Subtyping. I Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag. 2019. s. 356-371. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 11200 LNCS). doi: 10.1007/978-3-030-22348-9_21

Bessai, Jan ; Rehof, Jakob ; Düdder, Boris. / Fast Verified BCD Subtyping. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag, 2019. s. 356-371 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 11200 LNCS).

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

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "356--371",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

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

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 356

EP - 371

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

PB - Springer Verlag

ER -