3 Search Results for "Xu, Han"

Document
Artifact
DOI: 10.4230/DARTS.8.2.4
Direct Foundations for Compositional Programming (Artifact)

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

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

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

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)

Copy BibTex To Clipboard

@Article{fan_et_al:DARTS.8.2.4,
  author =	{Fan, Andong and Huang, Xuejing and Xu, Han and Sun, Yaozhu and Oliveira, Bruno C. d. S.},
  title =	{{Direct Foundations for Compositional Programming (Artifact)}},
  pages =	{4:1--4:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Fan, Andong and Huang, Xuejing and Xu, Han and Sun, Yaozhu and Oliveira, Bruno C. d. S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.4},
  URN =		{urn:nbn:de:0030-drops-162020},
  doi =		{10.4230/DARTS.8.2.4},
  annote =	{Keywords: Intersection types, disjoint polymorphism, operational semantics}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.18
Direct Foundations for Compositional Programming

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

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
The recently proposed CP language adopts Compositional Programming: a new modular programming style that solves challenging problems such as the Expression Problem. CP is implemented on top of a polymorphic core language with disjoint intersection types called 𝖥_{i}^{+}. The semantics of 𝖥_{i}^{+} employs an elaboration to a target language and relies on a sophisticated proof technique to prove the coherence of the elaboration. Unfortunately, the proof technique is technically challenging and hard to scale to many common features, including recursion or impredicative polymorphism. Thus, the original formulation of 𝖥_{i}^{+} does not support the two later features, which creates a gap between theory and practice, since CP fundamentally relies on them. This paper presents a new formulation of 𝖥_{i}^{+} based on a type-directed operational semantics (TDOS). The TDOS approach was recently proposed to model the semantics of languages with disjoint intersection types (but without polymorphism). Our work shows that the TDOS approach can be extended to languages with disjoint polymorphism and model the full 𝖥_{i}^{+} calculus. Unlike the elaboration semantics, which gives the semantics to 𝖥_{i}^{+} indirectly via a target language, the TDOS approach gives a semantics to 𝖥_{i}^{+} directly. With a TDOS, there is no need for a coherence proof. Instead, we can simply prove that the semantics is deterministic. The proof of determinism only uses simple reasoning techniques, such as straightforward induction, and is able to handle problematic features such as recursion and impredicative polymorphism. This removes the gap between theory and practice and validates the original proofs of correctness for CP. We formalized the TDOS variant of the 𝖥_{i}^{+} calculus and all its proofs in the Coq proof assistant.
Cite as

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 18:1-18:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{fan_et_al:LIPIcs.ECOOP.2022.18,
  author =	{Fan, Andong and Huang, Xuejing and Xu, Han and Sun, Yaozhu and Oliveira, Bruno C. d. S.},
  title =	{{Direct Foundations for Compositional Programming}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{18:1--18:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.18},
  URN =		{urn:nbn:de:0030-drops-162463},
  doi =		{10.4230/LIPIcs.ECOOP.2022.18},
  annote =	{Keywords: Intersection types, disjoint polymorphism, operational semantics}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.143
Analytical Differential Calculus with Integration

Authors: Han Xu and Zhenjiang Hu

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
Differential lambda-calculus was first introduced by Thomas Ehrhard and Laurent Regnier in 2003. Despite more than 15 years of history, little work has been done on a differential calculus with integration. In this paper, we shall propose a differential calculus with integration from a programming point of view. We show its good correspondence with mathematics, which is manifested by how we construct these reduction rules and how we preserve important mathematical theorems in our calculus. Moreover, we highlight applications of the calculus in incremental computation, automatic differentiation, and computation approximation.
Cite as

Han Xu and Zhenjiang Hu. Analytical Differential Calculus with Integration. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 143:1-143:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{xu_et_al:LIPIcs.ICALP.2021.143,
  author =	{Xu, Han and Hu, Zhenjiang},
  title =	{{Analytical Differential Calculus with Integration}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{143:1--143:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.143},
  URN =		{urn:nbn:de:0030-drops-142127},
  doi =		{10.4230/LIPIcs.ICALP.2021.143},
  annote =	{Keywords: Differential Calculus, Integration, Lambda Calculus, Incremental Computation, Adaptive Computing}
}
  • Refine by Author
  • 3 Xu, Han
  • 2 Fan, Andong
  • 2 Huang, Xuejing
  • 2 Oliveira, Bruno C. d. S.
  • 2 Sun, Yaozhu
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Type theory
  • 1 Software and its engineering → Functional languages
  • 1 Software and its engineering → General programming languages

  • Refine by Keyword
  • 2 Intersection types
  • 2 disjoint polymorphism
  • 2 operational semantics
  • 1 Adaptive Computing
  • 1 Differential Calculus
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 2 2022
  • 1 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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