Fast Verified BCD Subtyping
Research output: Chapter in Book/Report/Conference proceeding › Book chapter › Research › peer-review
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 | Models, Mindsets, Meta : The What, the How, and the Why Not? |
Editors | Tiziana Margaria, Susann Graf, Kim G. Larsen |
Number of pages | 16 |
Publisher | Springer |
Publication date | 1 Jan 2019 |
Pages | 356-371 |
ISBN (Print) | 978-3-030-22347-2 |
ISBN (Electronic) | 978-3-030-22348-9 |
DOIs | |
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 |
- BCD, Coq, Intersection types, Subtyping
Research areas
ID: 230703225