Fast Verified BCD Subtyping

Research output: Chapter in Book/Report/Conference proceedingBook chapterResearchpeer-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 languageEnglish
Title of host publicationModels, Mindsets, Meta : The What, the How, and the Why Not?
EditorsTiziana Margaria, Susann Graf, Kim G. Larsen
Number of pages16
PublisherSpringer
Publication date1 Jan 2019
Pages356-371
ISBN (Print)978-3-030-22347-2
ISBN (Electronic) 978-3-030-22348-9
DOIs
Publication statusPublished - 1 Jan 2019
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11200 LNCS
ISSN0302-9743

    Research areas

  • BCD, Coq, Intersection types, Subtyping

ID: 230703225