Document Open Access Logo

Direct Foundations for Compositional Programming (Artifact)

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

PDF

Artifact Description

Thumbnail PDF
PDF
DARTS.8.2.4.pdf
  • Filesize: 0.6 MB
  • 3 pages

Document Identifiers

Subject Classification

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

Metrics

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

Abstract

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.

Cite As Get 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) https://doi.org/10.4230/DARTS.8.2.4

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

Funding

This research was funded by the University of Hong Kong and Hong Kong Research Grants Council projects number 17209519, 17209520 and 17209821.

Acknowledgements

We thank the anonymous reviewers for their helpful comments.

Artifact

  MD5 Sum: 4afe79ce3b2bbb80e8f9d0e419d22922 (Get MD5 Sum)

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

Related Article

  • Andong Fan, Xuejing Huang, Han Xu, Yaozhu Sun, and Bruno C. d. S. Oliveira, "Direct Foundations for Compositional Programming", in 36th European Conference on Object-Oriented Programming (ECOOP 2022), LIPIcs, Vol. 222, pp. 18:1-18:28, 2022. https://doi.org/10.4230/LIPIcs.ECOOP.2022.18

References

  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: https://doi.org/10.1145/1328438.1328443.
  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: https://repository.upenn.edu/cis_reports/933/.
  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: https://www.chargueraud.org/softs/tlc/.
  5. The Coq Development Team. The Coq Reference Manual, version 8.11.1, April 2020. Available electronically at URL: https://coq.inria.fr/distrib/current/refman/.
  6. XUEJING HUANG, JINXU ZHAO, and BRUNO C. D. S. OLIVEIRA. Taming the merge operator. Journal of Functional Programming, 31:e28, 2021. URL: https://doi.org/10.1017/S0956796821000186.
  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. https://downloads.haskell.org/~ghc/latest/docs/users_guide.pdf, 2020.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact