DARTS.8.2.4.pdf
- Filesize: 0.6 MB
- 3 pages
Document
Direct Foundations for Compositional Programming (Artifact)
Authors
Andong Fan 
,
Xuejing Huang ,
Han Xu ,
-
Part of:
Issue:
Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)
Volume: DARTS, Volume 8 (ECOOP 2022)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2022-06-23
Artifact Description
Document Identifiers
Author Details
Acknowledgements
We thank the anonymous reviewers for their helpful comments.
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
Artifact
DARTS-8-2-4-artifact-4afe79ce3b2bbb80e8f9d0e419d22922.zip
(Filesize: 1.36 GB)
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
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.
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)
0PDF Downloads
References
- 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.
- 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/.
-
Arthur Charguéraud. The locally nameless representation. Journal of Automated Reasoning, 49(3):363-408, 2012.
- Arthur Charguéraud and François Pottier. Tlc: a non-constructive library for coq. URL: https://www.chargueraud.org/softs/tlc/.
- 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/.
- 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.
-
Dirk Merkel. Docker: lightweight linux containers for consistent development and deployment. Linux journal, 2014(239):2, 2014.
-
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.
- GHC Team. Ghc use’s guide documentation. https://downloads.haskell.org/~ghc/latest/docs/users_guide.pdf, 2020.