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 for this work

2 Citations (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.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Number of pages	16
Publisher	Springer Verlag
Publication date	1 Jan 2019
Pages	356-371
DOIs	https://doi.org/10.1007/978-3-030-22348-9_21
Publication status	Published - 1 Jan 2019

Series	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11200 LNCS
ISSN	0302-9743

Keywords

BCD
Coq
Intersection types
Subtyping

Access to Document

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

Cite this

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. 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

Bessai, J, Rehof, J & Düdder, B 2019, Fast Verified BCD Subtyping. in 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), vol. 11200 LNCS, pp. 356-371. https://doi.org/10.1007/978-3-030-22348-9_21

Bessai J, Rehof J, Düdder B. Fast Verified BCD Subtyping. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag. 2019. p. 356-371. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 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. pp. 356-371 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 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 -

Fast Verified BCD Subtyping

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this