Direct Foundations for Compositional Programming (Artifact)

Authors Andong Fan , Xuejing Huang , Han Xu , Yaozhu Sun, Bruno C. d. S. Oliveira

Thumbnail PDF

Artifact Description

  • Filesize: 0.6 MB
  • 3 pages

Document Identifiers

Author Details

Andong Fan
  • Zhejiang University, Hangzhou, China
Xuejing Huang
  • The University of Hong Kong, China
Han Xu
  • Peking University, Beijing, China
Yaozhu Sun
  • The University of Hong Kong, China
Bruno C. d. S. Oliveira
  • The University of Hong Kong, China


We thank the anonymous reviewers for their helpful comments.

Cite AsGet BibTex

Andong Fan, Xuejing Huang, Han Xu, Yaozhu Sun, and Bruno C. d. S. Oliveira. Direct Foundations for Compositional Programming (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 4:1-4:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2022 Call for Artifacts and the ACM Artifact Review and Badging Policy


Our companion paper proposes a new formulation of the 𝖥_{i}^{+} calculus with disjoint polymorphism and a merge operator based on Type-Directed Operational Semantics. The artifact contains Coq formalization of the 𝖥_{i}^{+} calculus and our new implementation of the CP language, which demonstrates the new 𝖥_{i}^{+} can serve as the direct foundation for Compositional Programming.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Intersection types
  • disjoint polymorphism
  • operational semantics


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. Engineering formal metatheory. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '08, pages 3-15, New York, NY, USA, 2008. Association for Computing Machinery. URL:
  2. Brian Aydemir and Stephanie Weirich. Lngen: Tool support for locally nameless representations. Technical Report MS-CIS-10-24, Department of Computer and Information Science, University of Pennsylvania, June 2010. URL:
  3. Arthur Charguéraud. The locally nameless representation. Journal of Automated Reasoning, 49(3):363-408, 2012. Google Scholar
  4. Arthur Charguéraud and François Pottier. Tlc: a non-constructive library for coq. URL:
  5. The Coq Development Team. The Coq Reference Manual, version 8.11.1, April 2020. Available electronically at URL:
  6. XUEJING HUANG, JINXU ZHAO, and BRUNO C. D. S. OLIVEIRA. Taming the merge operator. Journal of Functional Programming, 31:e28, 2021. URL:
  7. Dirk Merkel. Docker: lightweight linux containers for consistent development and deployment. Linux journal, 2014(239):2, 2014. Google Scholar
  8. Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, et al. Ott: Effective tool support for the working semanticist. Journal of functional programming, 20(1):71-122, 2010. Google Scholar
  9. GHC Team. Ghc use’s guide documentation., 2020.