7 Search Results for "Ye, Hong"


Document
Short Paper
Predicting visit frequencies to new places (Short Paper)

Authors: Nina Wiedemann, Ye Hong, and Martin Raubal

Published in: LIPIcs, Volume 277, 12th International Conference on Geographic Information Science (GIScience 2023)


Abstract
Human mobility exhibits power-law distributed visitation patterns; i.e., a few locations are visited frequently and many locations only once. Current research focuses on the important locations of users or on recommending new places based on collective behaviour, neglecting the existence of scarcely visited locations. However, assessing whether a user will return to a location in the future is highly relevant for personalized location-based services. Therefore, we propose a new problem formulation aimed at predicting the future visit frequency to a new location, focusing on the previous mobility behaviour of a single user. Our preliminary results demonstrate that visit frequency prediction is a difficult task, but sophisticated learning models can detect insightful patterns in the historic mobility indicative of future visit frequency. We believe these models can uncover valuable insights into the spatial factors that drive individual mobility behaviour.

Cite as

Nina Wiedemann, Ye Hong, and Martin Raubal. Predicting visit frequencies to new places (Short Paper). In 12th International Conference on Geographic Information Science (GIScience 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 277, pp. 84:1-84:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{wiedemann_et_al:LIPIcs.GIScience.2023.84,
  author =	{Wiedemann, Nina and Hong, Ye and Raubal, Martin},
  title =	{{Predicting visit frequencies to new places}},
  booktitle =	{12th International Conference on Geographic Information Science (GIScience 2023)},
  pages =	{84:1--84:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-288-4},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{277},
  editor =	{Beecham, Roger and Long, Jed A. and Smith, Dianna and Zhao, Qunshan and Wise, Sarah},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.GIScience.2023.84},
  URN =		{urn:nbn:de:0030-drops-189794},
  doi =		{10.4230/LIPIcs.GIScience.2023.84},
  annote =	{Keywords: Human mobility, Visitation patterns, Place recommendation, Next location prediction}
}
Document
Compositional Verification of Interacting Systems Using Event Monads

Authors: Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, and Bican Xia

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)


Abstract
Large software systems are usually divided into multiple components that interact with each other. How to verify interacting components in a modular way is one of the major problems in formal verification. In many cases, interaction between components can be modeled asynchronously, where events are sent without requiring a response in order to continue with execution of the component. In this paper, we propose a lightweight, event-based framework for verification of components with asynchronous interaction. We define event monads and event systems, and a Hoare logic-style calculus for reasoning about them. The framework is implemented in Isabelle and applied to several case studies, including models for distributed computing, cache-coherence protocols, and verification of partition scheduling in a real-time operating system.

Cite as

Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, and Bican Xia. Compositional Verification of Interacting Systems Using Event Monads. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{zhan_et_al:LIPIcs.ITP.2022.33,
  author =	{Zhan, Bohua and Lv, Yi and Wang, Shuling and Zhao, Gehang and Hao, Jifeng and Ye, Hong and Xia, Bican},
  title =	{{Compositional Verification of Interacting Systems Using Event Monads}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{33:1--33:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.33},
  URN =		{urn:nbn:de:0030-drops-167420},
  doi =		{10.4230/LIPIcs.ITP.2022.33},
  annote =	{Keywords: Hoare Logic, Compositional Verification, Events}
}
Document
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
A Clustering-Based Framework for Individual Travel Behaviour Change Detection

Authors: Ye Hong, Yanan Xin, Henry Martin, Dominik Bucher, and Martin Raubal

Published in: LIPIcs, Volume 208, 11th International Conference on Geographic Information Science (GIScience 2021) - Part II


Abstract
The emergence of passively and continuously recorded movement data offers new opportunities to study the long-term change of individual travel behaviour from data-driven perspectives. This study proposes a clustering-based framework to identify travel behaviour patterns and detect potential change periods on the individual level. First, we extract important trips that depict individual characteristic movement. Then, considering trip mode, trip distance, and trip duration as travel behaviour dimensions, we measure the similarities of trips and group them into clusters using hierarchical clustering. The trip clusters represent dimensions of travel behaviours, and the change of their relative proportions over time reflect the development of travel preferences. We use two different methods to detect changes in travel behaviour patterns: the Herfindahl-Hirschman index-based method and the sliding window-based method. The framework is tested using data from a large-scale longitudinal GPS tracking data study in which participants had access to a Mobility-as-a-Service (MaaS) offer. The methods successfully identify significant travel behaviour changes for users. Moreover, we analyse the impact of the MaaS offer on individual travel behaviours with the obtained change information. The proposed framework for behaviour change detection provides valuable insights for travel demand management and evaluating people’s reactions to sustainable mobility options.

Cite as

Ye Hong, Yanan Xin, Henry Martin, Dominik Bucher, and Martin Raubal. A Clustering-Based Framework for Individual Travel Behaviour Change Detection. In 11th International Conference on Geographic Information Science (GIScience 2021) - Part II. Leibniz International Proceedings in Informatics (LIPIcs), Volume 208, pp. 4:1-4:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{hong_et_al:LIPIcs.GIScience.2021.II.4,
  author =	{Hong, Ye and Xin, Yanan and Martin, Henry and Bucher, Dominik and Raubal, Martin},
  title =	{{A Clustering-Based Framework for Individual Travel Behaviour Change Detection}},
  booktitle =	{11th International Conference on Geographic Information Science (GIScience 2021) - Part II},
  pages =	{4:1--4:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-208-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{208},
  editor =	{Janowicz, Krzysztof and Verstegen, Judith A.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.GIScience.2021.II.4},
  URN =		{urn:nbn:de:0030-drops-147635},
  doi =		{10.4230/LIPIcs.GIScience.2021.II.4},
  annote =	{Keywords: Human mobility, Travel behaviour, Change detection, Trip clustering}
}
Document
Artifact
Type-Directed Operational Semantics for Gradual Typing (Artifact)

Authors: Wenjia Ye, Bruno C. d. S. Oliveira, and Xuejing Huang

Published in: DARTS, Volume 7, Issue 2, Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021)


Abstract
This artifact includes the Coq formalization associated with the paper Type-Directed Operational Semantics for Gradual Typing submitted in ECOOP 2021. The paper illustrates how to employ TDOS on gradually typed languages using two calculi. The first calculus, called λB, is inspired by the semantics of the blame calculus(λB^g) and is sound with λB^g. The second calculus, called λB^r, explores a different design space in the semantics of gradually typed languages. This document explains how to run the Coq formalization. Artifact can either be compiled in the pre-built docker image with all the dependencies installed or it could be built from the scratch. Sections 1-7 explain the basic information about the artifact. Section 7 explains how to get the docker image for the artifact. Section 8 explains the prerequisites and the steps to run coq files from scratch. Section 9 explains coq files briefly. Section 10 shows the correspondence of important lemmas, definitions and pictures discussed in the paper with their respective Coq formalization.

Cite as

Wenjia Ye, Bruno C. d. S. Oliveira, and Xuejing Huang. Type-Directed Operational Semantics for Gradual Typing (Artifact). In Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021). Dagstuhl Artifacts Series (DARTS), Volume 7, Issue 2, pp. 9:1-9:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@Article{ye_et_al:DARTS.7.2.9,
  author =	{Ye, Wenjia and Oliveira, Bruno C. d. S. and Huang, Xuejing},
  title =	{{Type-Directed Operational Semantics for Gradual Typing (Artifact)}},
  pages =	{9:1--9:6},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2021},
  volume =	{7},
  number =	{2},
  editor =	{Ye, Wenjia and Oliveira, Bruno C. d. S. and Huang, Xuejing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.7.2.9},
  URN =		{urn:nbn:de:0030-drops-140337},
  doi =		{10.4230/DARTS.7.2.9},
  annote =	{Keywords: Gradual Typing, Operational Semantics, Type Systems}
}
Document
Type-Directed Operational Semantics for Gradual Typing

Authors: Wenjia Ye, Bruno C. d. S. Oliveira, and Xuejing Huang

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)


Abstract
The semantics of gradually typed languages is typically given indirectly via an elaboration into a cast calculus. This contrasts with more conventional formulations of programming language semantics, where the semantics of a language is given directly using, for instance, an operational semantics. This paper presents a new approach to give the semantics of gradually typed languages directly. We use a recently proposed variant of small-step operational semantics called type-directed operational semantics (TDOS). In TDOS type annotations become operationally relevant and can affect the result of a program. In the context of a gradually typed language, such type annotations are used to trigger type-based conversions on values. We illustrate how to employ TDOS on gradually typed languages using two calculi. The first calculus, called λ B^g, is inspired by the semantics of the blame calculus, but it has implicit type conversions, enabling it to be used as a gradually typed language. The second calculus, called λ B^r, explores a different design space in the semantics of gradually typed languages. It uses a so-called blame recovery semantics, which enables eliminating some false positives where blame is raised but normal computation could succeed. For both calculi, type safety is proved. Furthermore we show that the semantics of λ B^g is sound with respect to the semantics of the blame calculus, and that λ B^r comes with a gradual guarantee. All the results have been mechanically formalized in the Coq theorem prover.

Cite as

Wenjia Ye, Bruno C. d. S. Oliveira, and Xuejing Huang. Type-Directed Operational Semantics for Gradual Typing. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 12:1-12:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{ye_et_al:LIPIcs.ECOOP.2021.12,
  author =	{Ye, Wenjia and Oliveira, Bruno C. d. S. and Huang, Xuejing},
  title =	{{Type-Directed Operational Semantics for Gradual Typing}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{12:1--12:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.12},
  URN =		{urn:nbn:de:0030-drops-140551},
  doi =		{10.4230/LIPIcs.ECOOP.2021.12},
  annote =	{Keywords: Gradual Typing, Type Systems, Operational Semantics}
}
Document
A Polynomial Kernel for Diamond-Free Editing

Authors: Yixin Cao, Ashutosh Rai, R. B. Sandeep, and Junjie Ye

Published in: LIPIcs, Volume 112, 26th Annual European Symposium on Algorithms (ESA 2018)


Abstract
Given a fixed graph H, the H-free editing problem asks whether we can edit at most k edges to make a graph contain no induced copy of H. We obtain a polynomial kernel for this problem when H is a diamond. The incompressibility dichotomy for H being a 3-connected graph and the classical complexity dichotomy suggest that except for H being a complete/empty graph, H-free editing problems admit polynomial kernels only for a few small graphs H. Therefore, we believe that our result is an essential step toward a complete dichotomy on the compressibility of H-free editing. Additionally, we give a cubic-vertex kernel for the diamond-free edge deletion problem, which is far simpler than the previous kernel of the same size for the problem.

Cite as

Yixin Cao, Ashutosh Rai, R. B. Sandeep, and Junjie Ye. A Polynomial Kernel for Diamond-Free Editing. In 26th Annual European Symposium on Algorithms (ESA 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 112, pp. 10:1-10:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{cao_et_al:LIPIcs.ESA.2018.10,
  author =	{Cao, Yixin and Rai, Ashutosh and Sandeep, R. B. and Ye, Junjie},
  title =	{{A Polynomial Kernel for Diamond-Free Editing}},
  booktitle =	{26th Annual European Symposium on Algorithms (ESA 2018)},
  pages =	{10:1--10:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-081-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{112},
  editor =	{Azar, Yossi and Bast, Hannah and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2018.10},
  URN =		{urn:nbn:de:0030-drops-94732},
  doi =		{10.4230/LIPIcs.ESA.2018.10},
  annote =	{Keywords: Kernelization, Diamond-free, H-free editing, Graph modification problem}
}
  • Refine by Author
  • 3 Huang, Xuejing
  • 3 Oliveira, Bruno C. d. S.
  • 2 Hong, Ye
  • 2 Raubal, Martin
  • 2 Ye, Wenjia
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Type theory
  • 2 Applied computing → Transportation
  • 2 Information systems → Geographic information systems
  • 2 Software and its engineering → Object oriented languages
  • 2 Software and its engineering → Polymorphism
  • Show More...

  • Refine by Keyword
  • 2 Gradual Typing
  • 2 Human mobility
  • 2 Operational Semantics
  • 2 Type Systems
  • 1 Change detection
  • Show More...

  • Refine by Type
  • 7 document

  • Refine by Publication Year
  • 3 2021
  • 2 2022
  • 1 2018
  • 1 2023

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