10 Search Results for "Liu, Yu"


Document
Extended Abstract
Vincent: Green Hot Methods in the JVM (Extended Abstract)

Authors: Kenan Liu, Khaled Mahmoud, Joonhwan Yoo, and Yu David Liu

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


Abstract
In this paper, we show the energy efficiency of Java applications can be improved by applying Dynamic Voltage and Frequency Scaling (DVFS) inside the Java Virtual Machine (JVM). We augment the JVM to record the energy consumption of hot methods as the underlying CPU is run at different clock frequencies; after all the frequency possibilities for a method have been explored, the execution of the method in an optimized run is set to the CPU frequency that leads to the most energy-efficient execution for that method. We introduce a new sampling methodology to overcome the dual challenges in our design: both the underlying measurement mechanism for energy profiling and the DVFS for energy optimization are overhead-prone. We extend JikesRVM with our approach and benchmark it over the DaCapo suite on a server-class Linux machine. Experiments show we are able to use 14.9% less energy than built-in power management in Linux, and improve energy efficiency by 21.1% w.r.t. the metric of Energy-Delay Product (EDP).

Cite as

Kenan Liu, Khaled Mahmoud, Joonhwan Yoo, and Yu David Liu. Vincent: Green Hot Methods in the JVM (Extended Abstract). In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 32:1-32:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{liu_et_al:LIPIcs.ECOOP.2022.32,
  author =	{Liu, Kenan and Mahmoud, Khaled and Yoo, Joonhwan and Liu, Yu David},
  title =	{{Vincent: Green Hot Methods in the JVM}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{32:1--32:30},
  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.32},
  URN =		{urn:nbn:de:0030-drops-162605},
  doi =		{10.4230/LIPIcs.ECOOP.2022.32},
  annote =	{Keywords: energy efficiency, JVM, just-in-time compilation}
}
Document
Enumeration of d-Combining Tree-Child Networks

Authors: Yu-Sheng Chang, Michael Fuchs, Hexuan Liu, Michael Wallner, and Guan-Ru Yu

Published in: LIPIcs, Volume 225, 33rd International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms (AofA 2022)


Abstract
Tree-child networks are one of the most prominent network classes for modeling evolutionary processes which contain reticulation events. Several recent studies have addressed counting questions for bicombining tree-child networks which are tree-child networks with every reticulation node having exactly two parents. In this paper, we extend these studies to d-combining tree-child networks where every reticulation node has now d ≥ 2 parents. Moreover, we also give results and conjectures on the distributional behavior of the number of reticulation nodes of a network which is drawn uniformly at random from the set of all tree-child networks with the same number of leaves.

Cite as

Yu-Sheng Chang, Michael Fuchs, Hexuan Liu, Michael Wallner, and Guan-Ru Yu. Enumeration of d-Combining Tree-Child Networks. In 33rd International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms (AofA 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 225, pp. 5:1-5:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{chang_et_al:LIPIcs.AofA.2022.5,
  author =	{Chang, Yu-Sheng and Fuchs, Michael and Liu, Hexuan and Wallner, Michael and Yu, Guan-Ru},
  title =	{{Enumeration of d-Combining Tree-Child Networks}},
  booktitle =	{33rd International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms (AofA 2022)},
  pages =	{5:1--5:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-230-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{225},
  editor =	{Ward, Mark Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.AofA.2022.5},
  URN =		{urn:nbn:de:0030-drops-160914},
  doi =		{10.4230/LIPIcs.AofA.2022.5},
  annote =	{Keywords: Phylogenetic network, tree-child network, d-combining tree-child network, exact enumeration, asymptotic enumeration, reticulation node, limit law, stretched exponential}
}
Document
Skiing Is Easy, Gymnastics Is Hard: Complexity of Routine Construction in Olympic Sports

Authors: James Koppel and Yun William Yu

Published in: LIPIcs, Volume 226, 11th International Conference on Fun with Algorithms (FUN 2022)


Abstract
Some Olympic sports, like the marathon, are purely feats of human athleticism. But in others such as gymnastics, athletes channel their athleticism into a routine of skills. In these disciplines, designing the highest-scoring routine can be a challenging problem, because the routines are judged via a combination of artistic merit, which is largely subjective, and technical difficulty, which comes with complicated but objective scoring rules. Notably, since the 2006 Code of Points, FIG (International Gymnastics Federation) has sought to make gymnastics scoring more objective by encoding more of the score in those objective technical side of scoring, and in this paper, we show how that push is reflected in the computational complexity of routine optimization. Here, we analyze the purely-technical component of the scoring rules of routines in 17 different events across 5 Olympic sports. We identify four attributes that classify the common rules found in scoring functions, and, for each combination of attributes, prove hardness results or provide algorithms for designing the highest-scoring routine according to the objective technical component of the scoring functions. Ultimately, we discover that optimal routine construction for events in artistic, rhythmic, and trampoline gymnastics is NP-hard, while optimal routine construction for all other sports is in P.

Cite as

James Koppel and Yun William Yu. Skiing Is Easy, Gymnastics Is Hard: Complexity of Routine Construction in Olympic Sports. In 11th International Conference on Fun with Algorithms (FUN 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 226, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{koppel_et_al:LIPIcs.FUN.2022.17,
  author =	{Koppel, James and Yu, Yun William},
  title =	{{Skiing Is Easy, Gymnastics Is Hard: Complexity of Routine Construction in Olympic Sports}},
  booktitle =	{11th International Conference on Fun with Algorithms (FUN 2022)},
  pages =	{17:1--17:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-232-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{226},
  editor =	{Fraigniaud, Pierre and Uno, Yushi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FUN.2022.17},
  URN =		{urn:nbn:de:0030-drops-159877},
  doi =		{10.4230/LIPIcs.FUN.2022.17},
  annote =	{Keywords: complexity, games, sports}
}
Document
Canonical Solutions to Recursive Equations and Completeness of Equational Axiomatisations

Authors: Xinxin Liu and TingTing Yu

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)


Abstract
In this paper we prove completeness of four axiomatisations for finite-state behaviours with respect to behavioural equivalences at various τ-abstract levels: branching congruence, delay congruence, η-congruence, and weak congruence. Instead of merging guarded recursive equations, which was the approach originally used by Robin Milner and has since become the standard strategy for proving completeness results of this kind, in this work we take a new approach by solving guarded recursive equations with canonical solutions which are those with the fewest reachable states. The new strategy allows uniform treatment of the axiomatisations with respect to different behavioural equivalences.

Cite as

Xinxin Liu and TingTing Yu. Canonical Solutions to Recursive Equations and Completeness of Equational Axiomatisations. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 35:1-35:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{liu_et_al:LIPIcs.CONCUR.2020.35,
  author =	{Liu, Xinxin and Yu, TingTing},
  title =	{{Canonical Solutions to Recursive Equations and Completeness of Equational Axiomatisations}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{35:1--35:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.35},
  URN =		{urn:nbn:de:0030-drops-128479},
  doi =		{10.4230/LIPIcs.CONCUR.2020.35},
  annote =	{Keywords: Bisimulation, Congruence, Axiomatisation, Soundness and Completeness}
}
Document
Approximability of the Eight-Vertex Model

Authors: Jin-Yi Cai, Tianyu Liu, Pinyan Lu, and Jing Yu

Published in: LIPIcs, Volume 169, 35th Computational Complexity Conference (CCC 2020)


Abstract
We initiate a study of the classification of approximation complexity of the eight-vertex model defined over 4-regular graphs. The eight-vertex model, together with its special case the six-vertex model, is one of the most extensively studied models in statistical physics, and can be stated as a problem of counting weighted orientations in graph theory. Our result concerns the approximability of the partition function on all 4-regular graphs, classified according to the parameters of the model. Our complexity results conform to the phase transition phenomenon from physics. We introduce a quantum decomposition of the eight-vertex model and prove a set of closure properties in various regions of the parameter space. Furthermore, we show that there are extra closure properties on 4-regular planar graphs. These regions of the parameter space are concordant with the phase transition threshold. Using these closure properties, we derive polynomial time approximation algorithms via Markov chain Monte Carlo. We also show that the eight-vertex model is NP-hard to approximate on the other side of the phase transition threshold.

Cite as

Jin-Yi Cai, Tianyu Liu, Pinyan Lu, and Jing Yu. Approximability of the Eight-Vertex Model. In 35th Computational Complexity Conference (CCC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 169, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{cai_et_al:LIPIcs.CCC.2020.4,
  author =	{Cai, Jin-Yi and Liu, Tianyu and Lu, Pinyan and Yu, Jing},
  title =	{{Approximability of the Eight-Vertex Model}},
  booktitle =	{35th Computational Complexity Conference (CCC 2020)},
  pages =	{4:1--4:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-156-6},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{169},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2020.4},
  URN =		{urn:nbn:de:0030-drops-125564},
  doi =		{10.4230/LIPIcs.CCC.2020.4},
  annote =	{Keywords: Approximate complexity, the eight-vertex model, Markov chain Monte Carlo}
}
Document
Track A: Algorithms, Complexity and Games
Succinct Filters for Sets of Unknown Sizes

Authors: Mingmou Liu, Yitong Yin, and Huacheng Yu

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)


Abstract
The membership problem asks to maintain a set S ⊆ [u], supporting insertions and membership queries, i.e., testing if a given element is in the set. A data structure that computes exact answers is called a dictionary. When a (small) false positive rate ε is allowed, the data structure is called a filter. The space usages of the standard dictionaries or filters usually depend on the upper bound on the size of S, while the actual set can be much smaller. Pagh, Segev and Wieder [Pagh et al., 2013] were the first to study filters with varying space usage based on the current |S|. They showed in order to match the space with the current set size n = |S|, any filter data structure must use (1-o(1))n(log(1/ε)+(1-O(ε))log log n) bits, in contrast to the well-known lower bound of N log(1/ε) bits, where N is an upper bound on |S|. They also presented a data structure with almost optimal space of (1+o(1))n(log(1/ε)+O(log log n)) bits provided that n > u^0.001, with expected amortized constant insertion time and worst-case constant lookup time. In this work, we present a filter data structure with improvements in two aspects: - it has constant worst-case time for all insertions and lookups with high probability; - it uses space (1+o(1))n(log (1/ε)+log log n) bits when n > u^0.001, achieving optimal leading constant for all ε = o(1). We also present a dictionary that uses (1+o(1))nlog(u/n) bits of space, matching the optimal space in terms of the current size, and performs all operations in constant time with high probability.

Cite as

Mingmou Liu, Yitong Yin, and Huacheng Yu. Succinct Filters for Sets of Unknown Sizes. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 79:1-79:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{liu_et_al:LIPIcs.ICALP.2020.79,
  author =	{Liu, Mingmou and Yin, Yitong and Yu, Huacheng},
  title =	{{Succinct Filters for Sets of Unknown Sizes}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{79:1--79:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.79},
  URN =		{urn:nbn:de:0030-drops-124867},
  doi =		{10.4230/LIPIcs.ICALP.2020.79},
  annote =	{Keywords: Bloom filters, Data structures, Approximate set membership, Dictionaries}
}
Document
Track A: Algorithms, Complexity and Games
Optimal Short Cycle Decomposition in Almost Linear Time

Authors: Merav Parter and Eylon Yogev

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)


Abstract
Short cycle decomposition is an edge partitioning of an unweighted graph into edge-disjoint short cycles, plus a small number of extra edges not in any cycle. This notion was introduced by Chu et al. [FOCS'18] as a fundamental tool for graph sparsification and sketching. Clearly, it is most desirable to have a fast algorithm for partitioning the edges into as short as possible cycles, while omitting few edges. The most naïve procedure for such decomposition runs in time O(m * n) and partitions the edges into O(log n)-length edge-disjoint cycles plus at most 2n edges. Chu et al. improved the running time considerably to m^{1+o(1)}, while increasing both the length of the cycles and the number of omitted edges by a factor of n^{o(1)}. Even more recently, Liu-Sachdeva-Yu [SODA'19] showed that for every constant delta in (0,1] there is an O(m * n^{delta})-time algorithm that provides, w.h.p., cycles of length O(log n)^{1/delta} and O(n) extra edges. In this paper, we significantly improve upon these bounds. We first show an m^{1+o(1)}-time deterministic algorithm for computing nearly optimal cycle decomposition, i.e., with cycle length O(log^2 n) and an extra subset of O(n log n) edges not in any cycle. This algorithm is based on a reduction to low-congestion cycle covers, introduced by the authors in [SODA'19]. We also provide a simple deterministic algorithm that computes edge-disjoint cycles of length 2^{1/epsilon} with n^{1+epsilon}* 2^{1/epsilon} extra edges, for every epsilon in (0,1]. Combining this with Liu-Sachdeva-Yu [SODA'19] gives a linear time randomized algorithm for computing cycles of length poly(log n) and O(n) extra edges, for every n-vertex graphs with n^{1+1/delta} edges for some constant delta. These decomposition algorithms lead to improvements in all the algorithmic applications of Chu et al. as well as to new distributed constructions.

Cite as

Merav Parter and Eylon Yogev. Optimal Short Cycle Decomposition in Almost Linear Time. In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 89:1-89:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{parter_et_al:LIPIcs.ICALP.2019.89,
  author =	{Parter, Merav and Yogev, Eylon},
  title =	{{Optimal Short Cycle Decomposition in Almost Linear Time}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{89:1--89:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.89},
  URN =		{urn:nbn:de:0030-drops-106653},
  doi =		{10.4230/LIPIcs.ICALP.2019.89},
  annote =	{Keywords: Cycle decomposition, low-congestion cycle cover, graph sparsification}
}
Document
Short Paper
An Analytical Framework for Understanding Urban Functionality from Human Activities (Short Paper)

Authors: Chaogui Kang and Yu Liu

Published in: LIPIcs, Volume 114, 10th International Conference on Geographic Information Science (GIScience 2018)


Abstract
The intertwined relationship between urban functionality and human activity has been widely recognized and quantified with the assistance of big geospatial data. In specific, urban land uses as an important facet of urban structure can be identified from spatiotemporal patterns of aggregate human activities. In this article, we propose a space, time and activity cuboid based analytical framework for clustering urban spaces into different categories of urban functionality based on the variation of activity intensity (T-fiber), mixture (A-fiber) and interaction (I- and O-fiber). The ability of the proposed framework is empirically evaluated by three case studies.

Cite as

Chaogui Kang and Yu Liu. An Analytical Framework for Understanding Urban Functionality from Human Activities (Short Paper). In 10th International Conference on Geographic Information Science (GIScience 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 114, pp. 38:1-38:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{kang_et_al:LIPIcs.GISCIENCE.2018.38,
  author =	{Kang, Chaogui and Liu, Yu},
  title =	{{An Analytical Framework for Understanding Urban Functionality from Human Activities}},
  booktitle =	{10th International Conference on Geographic Information Science (GIScience 2018)},
  pages =	{38:1--38:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-083-5},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{114},
  editor =	{Winter, Stephan and Griffin, Amy and Sester, Monika},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.GISCIENCE.2018.38},
  URN =		{urn:nbn:de:0030-drops-93668},
  doi =		{10.4230/LIPIcs.GISCIENCE.2018.38},
  annote =	{Keywords: Urban functionality, Human activity, STA cuboid, Spatiotemporal distribution, Clustering}
}
Document
Short Paper
Modelling Spatial Patterns Using Graph Convolutional Networks (Short Paper)

Authors: Di Zhu and Yu Liu

Published in: LIPIcs, Volume 114, 10th International Conference on Geographic Information Science (GIScience 2018)


Abstract
The understanding of geographical reality is a process of data representation and pattern discovery. Former studies mainly adopted continuous-field models to represent spatial variables and to investigate the underlying spatial continuity/heterogeneity in a regular spatial domain. In this article, we introduce a more generalized model based on graph convolutional neural networks that can capture the complex parameters of spatial patterns underlying graph-structured spatial data, which generally contain both Euclidean spatial information and non-Euclidean feature information. A trainable site-selection framework is proposed to demonstrate the feasibility of our model in geographic decision problems.

Cite as

Di Zhu and Yu Liu. Modelling Spatial Patterns Using Graph Convolutional Networks (Short Paper). In 10th International Conference on Geographic Information Science (GIScience 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 114, pp. 73:1-73:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{zhu_et_al:LIPIcs.GISCIENCE.2018.73,
  author =	{Zhu, Di and Liu, Yu},
  title =	{{Modelling Spatial Patterns Using Graph Convolutional Networks}},
  booktitle =	{10th International Conference on Geographic Information Science (GIScience 2018)},
  pages =	{73:1--73:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-083-5},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{114},
  editor =	{Winter, Stephan and Griffin, Amy and Sester, Monika},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.GISCIENCE.2018.73},
  URN =		{urn:nbn:de:0030-drops-94016},
  doi =		{10.4230/LIPIcs.GISCIENCE.2018.73},
  annote =	{Keywords: Spatial pattern, Graph convolution, Big geo-data, Deep neural networks, Urban configuration}
}
Document
Intensional Effect Polymorphism

Authors: Yuheng Long, Yu David Liu, and Hridesh Rajan

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)


Abstract
Type-and-effect systems are a powerful tool for program construction and verification. We describe intensional effect polymorphism, a new foundation for effect systems that integrates static and dynamic effect checking. Our system allows the effect of polymorphic code to be intensionally inspected through a lightweight notion of dynamic typing. When coupled with parametric polymorphism, the powerful system utilizes runtime information to enable precise effect reasoning, while at the same time retains strong type safety guarantees. We build our ideas on top of an imperative core calculus with regions. The technical innovations of our design include a relational notion of effect checking, the use of bounded existential types to capture the subtle interactions between static typing and dynamic typing, and a differential alignment strategy to achieve efficiency in dynamic typing. We demonstrate the applications of intensional effect polymorphism in concurrent programming, security, graphical user interface access, and memoization.

Cite as

Yuheng Long, Yu David Liu, and Hridesh Rajan. Intensional Effect Polymorphism. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 346-370, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{long_et_al:LIPIcs.ECOOP.2015.346,
  author =	{Long, Yuheng and Liu, Yu David and Rajan, Hridesh},
  title =	{{Intensional Effect Polymorphism}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{346--370},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.346},
  URN =		{urn:nbn:de:0030-drops-52213},
  doi =		{10.4230/LIPIcs.ECOOP.2015.346},
  annote =	{Keywords: intensional effect polymorphism, type system, hybrid typing}
}
  • Refine by Author
  • 2 Liu, Yu
  • 2 Liu, Yu David
  • 1 Cai, Jin-Yi
  • 1 Chang, Yu-Sheng
  • 1 Fuchs, Michael
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Design and analysis of algorithms
  • 1 General and reference → General literature
  • 1 Information systems → Geographic information systems
  • 1 Mathematics of computing → Discrete mathematics
  • 1 Software and its engineering → Software performance
  • Show More...

  • Refine by Keyword
  • 1 Approximate complexity
  • 1 Approximate set membership
  • 1 Axiomatisation
  • 1 Big geo-data
  • 1 Bisimulation
  • Show More...

  • Refine by Type
  • 10 document

  • Refine by Publication Year
  • 3 2020
  • 3 2022
  • 2 2018
  • 1 2015
  • 1 2019

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