Fast Verified BCD Subtyping
Publikation: Bidrag til bog/antologi/rapport › Bidrag til bog/antologi › Forskning › fagfællebedømt
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 | Models, Mindsets, Meta : The What, the How, and the Why Not? |
Redaktører | Tiziana Margaria, Susann Graf, Kim G. Larsen |
Antal sider | 16 |
Forlag | Springer |
Publikationsdato | 1 jan. 2019 |
Sider | 356-371 |
ISBN (Trykt) | 978-3-030-22347-2 |
ISBN (Elektronisk) | 978-3-030-22348-9 |
DOI | |
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 |
ID: 230703225