The artifact contains the Coq formalization of \name, a simple calculus with disjoint intersection types supporting nested subtyping and composition, as described in the companion paper.
@Article{bi_et_al:DARTS.4.3.5, author = {Bi, Xuan and Oliveira, Bruno C. d. S. and Schrijvers, Tom}, title = {{The Essence of Nested Composition (Artifact)}}, pages = {5:1--5:2}, journal = {Dagstuhl Artifacts Series}, ISSN = {2509-8195}, year = {2018}, volume = {4}, number = {3}, editor = {Bi, Xuan and Oliveira, Bruno C. d. S. and Schrijvers, Tom}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.5}, URN = {urn:nbn:de:0030-drops-92363}, doi = {10.4230/DARTS.4.3.5}, annote = {Keywords: nested composition, family polymorphism, intersection types, coherence} }
2dddf320ea677407b10949973a105eb4
(Get MD5 Sum)
Feedback for Dagstuhl Publishing