Search Results

Documents authored by Richter, R. Bruce



Richter, R. Bruce

Document
Extending Drawings of Graphs to Arrangements of Pseudolines

Authors: Alan Arroyo, Julien Bensmail, and R. Bruce Richter

Published in: LIPIcs, Volume 164, 36th International Symposium on Computational Geometry (SoCG 2020)


Abstract
In the recent study of crossing numbers, drawings of graphs that can be extended to an arrangement of pseudolines (pseudolinear drawings) have played an important role as they are a natural combinatorial extension of rectilinear (or straight-line) drawings. A characterization of the pseudolinear drawings of K_n was found recently. We extend this characterization to all graphs, by describing the set of minimal forbidden subdrawings for pseudolinear drawings. Our characterization also leads to a polynomial-time algorithm to recognize pseudolinear drawings and construct the pseudolines when it is possible.

Cite as

Alan Arroyo, Julien Bensmail, and R. Bruce Richter. Extending Drawings of Graphs to Arrangements of Pseudolines. In 36th International Symposium on Computational Geometry (SoCG 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 164, pp. 9:1-9:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{arroyo_et_al:LIPIcs.SoCG.2020.9,
  author =	{Arroyo, Alan and Bensmail, Julien and Richter, R. Bruce},
  title =	{{Extending Drawings of Graphs to Arrangements of Pseudolines}},
  booktitle =	{36th International Symposium on Computational Geometry (SoCG 2020)},
  pages =	{9:1--9:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-143-6},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{164},
  editor =	{Cabello, Sergio and Chen, Danny Z.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2020.9},
  URN =		{urn:nbn:de:0030-drops-121672},
  doi =		{10.4230/LIPIcs.SoCG.2020.9},
  annote =	{Keywords: graphs, graph drawings, geometric graph drawings, arrangements of pseudolines, crossing numbers, stretchability}
}

Richter, Alexander

Document
Fast Robust Shortest Path Computations

Authors: Christoph Hansknecht, Alexander Richter, and Sebastian Stiller

Published in: OASIcs, Volume 65, 18th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2018)


Abstract
We develop a fast method to compute an optimal robust shortest path in large networks like road networks, a fundamental problem in traffic and logistics under uncertainty. In the robust shortest path problem we are given an s-t-graph D(V,A) and for each arc a nominal length c(a) and a maximal increase d(a) of its length. We consider all scenarios in which for the increased lengths c(a) + bar{d}(a) we have bar{d}(a) <= d(a) and sum_{a in A} (bar{d}(a)/d(a)) <= Gamma. Each path is measured by the length in its worst-case scenario. A classic result [Bertsimas and Sim, 2003] minimizes this path length by solving (|A| + 1)-many shortest path problems. Easily, (|A| + 1) can be replaced by |Theta|, where Theta is the set of all different values d(a) and 0. Still, the approach remains impractical for large graphs. Using the monotonicity of a part of the objective we devise a Divide and Conquer method to evaluate significantly fewer values of Theta. This methods generalizes to binary linear robust problems. Specifically for shortest paths we derive a lower bound to speed-up the Divide and Conquer of Theta. The bound is based on carefully using previous shortest path computations. We combine the approach with non-preprocessing based acceleration techniques for Dijkstra adapted to the robust case. In a computational study we document the value of different accelerations tried in the algorithm engineering process. We also give an approximation scheme for the robust shortest path problem which computes a (1 + epsilon)-approximate solution requiring O(log(d^ / (1 + epsilon))) computations of the nominal problem where d^ := max d(A) / min (d(A)\{0}).

Cite as

Christoph Hansknecht, Alexander Richter, and Sebastian Stiller. Fast Robust Shortest Path Computations. In 18th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2018). Open Access Series in Informatics (OASIcs), Volume 65, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{hansknecht_et_al:OASIcs.ATMOS.2018.5,
  author =	{Hansknecht, Christoph and Richter, Alexander and Stiller, Sebastian},
  title =	{{Fast Robust Shortest Path Computations}},
  booktitle =	{18th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2018)},
  pages =	{5:1--5:21},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-096-5},
  ISSN =	{2190-6807},
  year =	{2018},
  volume =	{65},
  editor =	{Bornd\"{o}rfer, Ralf and Storandt, Sabine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2018.5},
  URN =		{urn:nbn:de:0030-drops-97100},
  doi =		{10.4230/OASIcs.ATMOS.2018.5},
  annote =	{Keywords: Graph Algorithms, Shortest Paths, Robust Optimization}
}
Document
Multi-Dimensional Commodity Covering for Tariff Selection in Transportation

Authors: Felix G. König, Jannik Matuschke, and Alexander Richter

Published in: OASIcs, Volume 25, 12th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (2012)


Abstract
In this paper, we study a multi-dimensional commodity covering problem, which we encountered as a subproblem in optimizing large scale transportation networks in logistics. The problem asks for a selection of containers for transporting a given set of commodities, each commodity having different extensions of properties such as weight or volume. Each container can be selected multiple times and is specified by a fixed charge and capacities in the relevant properties. The task is to find a cost minimal collection of containers and a feasible assignment of the demand to all selected containers. From theoretical point of view, by exploring similarities to the well known SetCover problem, we derive NP-hardness and see that the non-approximability result known for set cover also carries over to our problem. For practical applications we need very fast heuristics to be integrated into a meta-heuristic framework that - depending on the context - either provide feasible near optimal solutions or only estimate the cost value of an optimal solution. We develop and analyze a flexible family of greedy algorithms that meet these challenges. In order to find best-performing configurations for different requirements of the meta-heuristic framework, we provide an extensive computational study on random and real world instance sets obtained from our project partner 4flow AG. We outline a trade-off between running times and solution quality and conclude that the proposed methods achieve the accuracy and efficiency necessary for serving as a key ingredient in more complex meta-heuristics enabling the optimization of large-scale networks.

Cite as

Felix G. König, Jannik Matuschke, and Alexander Richter. Multi-Dimensional Commodity Covering for Tariff Selection in Transportation. In 12th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems. Open Access Series in Informatics (OASIcs), Volume 25, pp. 58-70, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@InProceedings{konig_et_al:OASIcs.ATMOS.2012.58,
  author =	{K\"{o}nig, Felix G. and Matuschke, Jannik and Richter, Alexander},
  title =	{{Multi-Dimensional Commodity Covering for Tariff Selection in Transportation}},
  booktitle =	{12th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems},
  pages =	{58--70},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-45-3},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{25},
  editor =	{Delling, Daniel and Liberti, Leo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2012.58},
  URN =		{urn:nbn:de:0030-drops-37034},
  doi =		{10.4230/OASIcs.ATMOS.2012.58},
  annote =	{Keywords: Covering, Heuristics, Transportation, Tariff Selection}
}

Richter, Yossi

Document
An improved algorithm for CIOQ switches

Authors: Yossi Azar and Yossi Richter

Published in: Dagstuhl Seminar Proceedings, Volume 5031, Algorithms for Optimization with Incomplete Information (2005)


Abstract
The problem of maximizing the weighted throughput in various switching settings has been intensively studied recently through competitive analysis. To date, the most general model that has been investigated is the standard CIOQ (Combined Input and Output Queued) switch architecture with internal fabric speedup $S \geq 1$. CIOQ switches, that comprise the backbone of packet routing networks, are $N \times N$ switches controlled by a switching policy that incorporates two components: Admission control and scheduling. An admission control strategy is essential to determine the packets stored in the FIFO queues in input and output ports, while the scheduling policy conducts the transfer of packets through the internal fabric, from input ports to output ports. The online problem of maximizing the total weighted throughput of CIOQ switches was recently investigated by Kesselman and Ros\'{e}n [SPAA03]. They presented two different online algorithms for the general problem that achieve non-constant competitive ratios (linear in either the speedup or the number of distinct values, or logarithmic in the value range). We introduce the first constant-competitive algorithm for the general case of the problem, with arbitrary speedup and packet values. Specifically, our algorithm is $8$-competitive, and is also simple and easy to implement.

Cite as

Yossi Azar and Yossi Richter. An improved algorithm for CIOQ switches. In Algorithms for Optimization with Incomplete Information. Dagstuhl Seminar Proceedings, Volume 5031, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)


Copy BibTex To Clipboard

@InProceedings{azar_et_al:DagSemProc.05031.4,
  author =	{Azar, Yossi and Richter, Yossi},
  title =	{{An improved algorithm for CIOQ switches}},
  booktitle =	{Algorithms for Optimization with Incomplete Information},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{5031},
  editor =	{Susanne Albers and Rolf H. M\"{o}hring and Georg Ch. Pflug and R\"{u}diger Schultz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05031.4},
  URN =		{urn:nbn:de:0030-drops-670},
  doi =		{10.4230/DagSemProc.05031.4},
  annote =	{Keywords: On-line algorithms, Competitive ratio, CIOQ Switch, Packet Switching, Buffer Management, Quality of Service.}
}

Richter, M. M.

Document
Computer Science Logic (Dagstuhl Seminar 9229)

Authors: Egon Börger, Yuri Gurevich, Hans Kleine-Büning, and M. M. Richter

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)


Abstract

Cite as

Egon Börger, Yuri Gurevich, Hans Kleine-Büning, and M. M. Richter. Computer Science Logic (Dagstuhl Seminar 9229). Dagstuhl Seminar Report 40, pp. 1-28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1992)


Copy BibTex To Clipboard

@TechReport{borger_et_al:DagSemRep.40,
  author =	{B\"{o}rger, Egon and Gurevich, Yuri and Kleine-B\"{u}ning, Hans and Richter, M. M.},
  title =	{{Computer Science Logic (Dagstuhl Seminar 9229)}},
  pages =	{1--28},
  ISSN =	{1619-0203},
  year =	{1992},
  type = 	{Dagstuhl Seminar Report},
  number =	{40},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.40},
  URN =		{urn:nbn:de:0030-drops-149288},
  doi =		{10.4230/DagSemRep.40},
}

Richter, Kai-Florian

Document
Short Paper
Assessing Perceived Route Difficulty in Environments with Different Complexity (Short Paper)

Authors: Arvid Horned, Zoe Falomir, and Kai-Florian Richter

Published in: LIPIcs, Volume 315, 16th International Conference on Spatial Information Theory (COSIT 2024)


Abstract
Today, anyone feeling lost in a city or unsure about how to navigate can use navigation services to look up routes to where they want to go. Current research investigating these services has primarily focused on how to find an appropriate route and how to best support navigation along it, and not how routes and the maps they are presented on are perceived. What makes one route look more difficult to navigate than another? And how does experience with using navigation services and maps in daily life influence how difficult a route is perceived to be? We explored these questions in a survey study where participants rated the perceived difficulty of pedestrian routes in ten different cities. The results show that routes in more complex urban environments were perceived as more complex than routes in easier environments. At least partly, perceived difficulty seems to follow earlier conceptualizations of route complexity, but open questions remain regarding the interplay of environmental structure, route properties, and the map representation.

Cite as

Arvid Horned, Zoe Falomir, and Kai-Florian Richter. Assessing Perceived Route Difficulty in Environments with Different Complexity (Short Paper). In 16th International Conference on Spatial Information Theory (COSIT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 315, pp. 29:1-29:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{horned_et_al:LIPIcs.COSIT.2024.29,
  author =	{Horned, Arvid and Falomir, Zoe and Richter, Kai-Florian},
  title =	{{Assessing Perceived Route Difficulty in Environments with Different Complexity}},
  booktitle =	{16th International Conference on Spatial Information Theory (COSIT 2024)},
  pages =	{29:1--29:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-330-0},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{315},
  editor =	{Adams, Benjamin and Griffin, Amy L. and Scheider, Simon and McKenzie, Grant},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2024.29},
  URN =		{urn:nbn:de:0030-drops-208444},
  doi =		{10.4230/LIPIcs.COSIT.2024.29},
  annote =	{Keywords: navigation complexity, perceived difficulty, route display, spatial cognition}
}
Document
You Are Not Alone: Path Search Models, Traffic, and Social Costs

Authors: Fateme Teimouri and Kai-Florian Richter

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


Abstract
Existing cognitively motivated path search models ignore that we are hardly ever alone when navigating through an environment. They neither account for traffic nor for the social costs that being routed through certain areas may incur. In this paper, we analyse the effects of "not being alone" on different path search models, in particular on fastest paths and least complex paths. We find a significant effect of aiming to avoid traffic on social costs, but interestingly only minor effects on path complexity when minimizing either traffic load or social costs. Further, we find that ignoring traffic in path search leads to significantly increased average traffic load for all tested models. We also present results of a combined model that accounts for complexity, traffic, and social costs at the same time. Overall, this research provides important insights into the behavior of path search models when optimizing for different aspects, and explores some ways of mitigating unwanted effects.

Cite as

Fateme Teimouri and Kai-Florian Richter. You Are Not Alone: Path Search Models, Traffic, and Social Costs. In 11th International Conference on Geographic Information Science (GIScience 2021) - Part I. Leibniz International Proceedings in Informatics (LIPIcs), Volume 177, pp. 14:1-14:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{teimouri_et_al:LIPIcs.GIScience.2021.I.14,
  author =	{Teimouri, Fateme and Richter, Kai-Florian},
  title =	{{You Are Not Alone: Path Search Models, Traffic, and Social Costs}},
  booktitle =	{11th International Conference on Geographic Information Science (GIScience 2021) - Part I},
  pages =	{14:1--14:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-166-5},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{177},
  editor =	{Janowicz, Krzysztof and Verstegen, Judith A.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.GIScience.2021.I.14},
  URN =		{urn:nbn:de:0030-drops-130496},
  doi =		{10.4230/LIPIcs.GIScience.2021.I.14},
  annote =	{Keywords: wayfinding, navigation complexity, spatial cognition, social costs}
}
Document
Vision Paper
The Future of Geographic Information Displays from GIScience, Cartographic, and Cognitive Science Perspectives (Vision Paper)

Authors: Tyler Thrash, Sara Lanini-Maggi, Sara I. Fabrikant, Sven Bertel, Annina Brügger, Sascha Credé, Cao Tri Do, Georg Gartner, Haosheng Huang, Stefan Münzer, and Kai-Florian Richter

Published in: LIPIcs, Volume 142, 14th International Conference on Spatial Information Theory (COSIT 2019)


Abstract
With the development of modern geovisual analytics tools, several researchers have emphasized the importance of understanding users' cognitive, perceptual, and affective tendencies for supporting spatial decisions with geographic information displays (GIDs). However, most recent technological developments have focused on support for navigation in terms of efficiency and effectiveness while neglecting the importance of spatial learning. In the present paper, we will envision the future of GIDs that also support spatial learning in the context of large-scale navigation. Specifically, we will illustrate the manner in which GIDs have been (in the past) and might be (in the future) designed to be context-responsive, personalized, and supportive for active spatial learning from three different perspectives (i.e., GIScience, cartography, and cognitive science). We will also explain why this approach is essential for preventing the technological infantilizing of society (i.e., the reduction of our capacity to make decisions without technological assistance). Although these issues are common to nearly all emerging digital technologies, we argue that these issues become especially relevant in consideration of a person’s current and future locations.

Cite as

Tyler Thrash, Sara Lanini-Maggi, Sara I. Fabrikant, Sven Bertel, Annina Brügger, Sascha Credé, Cao Tri Do, Georg Gartner, Haosheng Huang, Stefan Münzer, and Kai-Florian Richter. The Future of Geographic Information Displays from GIScience, Cartographic, and Cognitive Science Perspectives (Vision Paper). In 14th International Conference on Spatial Information Theory (COSIT 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 142, pp. 19:1-19:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{thrash_et_al:LIPIcs.COSIT.2019.19,
  author =	{Thrash, Tyler and Lanini-Maggi, Sara and Fabrikant, Sara I. and Bertel, Sven and Br\"{u}gger, Annina and Cred\'{e}, Sascha and Do, Cao Tri and Gartner, Georg and Huang, Haosheng and M\"{u}nzer, Stefan and Richter, Kai-Florian},
  title =	{{The Future of Geographic Information Displays from GIScience, Cartographic, and Cognitive Science Perspectives}},
  booktitle =	{14th International Conference on Spatial Information Theory (COSIT 2019)},
  pages =	{19:1--19:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-115-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{142},
  editor =	{Timpf, Sabine and Schlieder, Christoph and Kattenbeck, Markus and Ludwig, Bernd and Stewart, Kathleen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2019.19},
  URN =		{urn:nbn:de:0030-drops-111113},
  doi =		{10.4230/LIPIcs.COSIT.2019.19},
  annote =	{Keywords: visual displays, geographic information, cartography, cognitive science}
}

Richter, David

Document
Compiling with Arrays

Authors: David Richter, Timon Böhler, Pascal Weisenburger, and Mira Mezini

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)


Abstract
Linear algebra computations are foundational for neural networks and machine learning, often handled through arrays. While many functional programming languages feature lists and recursion, arrays in linear algebra demand constant-time access and bulk operations. To bridge this gap, some languages represent arrays as (eager) functions instead of lists. In this paper, we connect this idea to a formal logical foundation by interpreting functions as the usual negative types from polarized type theory, and arrays as the corresponding dual positive version of the function type. Positive types are defined to have a single elimination form whose computational interpretation is pattern matching. Just like (positive) product types bind two variables during pattern matching, (positive) array types bind variables with multiplicity during pattern matching. We follow a similar approach for Booleans by introducing conditionally-defined variables. The positive formulation for the array type enables us to combine typed partial evaluation and common subexpression elimination into an elegant algorithm whose result enjoys a property we call maximal fission, which we argue can be beneficial for further optimizations. For this purpose, we present the novel intermediate representation indexed administrative normal form (A_{i}NF), which relies on the formal logical foundation of the positive formulation for the array type to facilitate maximal loop fission and subsequent optimizations. A_{i}NF is normal with regard to commuting conversion for both let-bindings and for-loops, leading to flat and maximally fissioned terms. We mechanize the translation and normalization from a simple surface language to A_{i}NF, establishing that the process terminates, preserves types, and produces maximally fissioned terms.

Cite as

David Richter, Timon Böhler, Pascal Weisenburger, and Mira Mezini. Compiling with Arrays. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 33:1-33:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{richter_et_al:LIPIcs.ECOOP.2024.33,
  author =	{Richter, David and B\"{o}hler, Timon and Weisenburger, Pascal and Mezini, Mira},
  title =	{{Compiling with Arrays}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{33:1--33:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.33},
  URN =		{urn:nbn:de:0030-drops-208823},
  doi =		{10.4230/LIPIcs.ECOOP.2024.33},
  annote =	{Keywords: array languages, functional programming, domain-specific languages, normalization by evaluation, common subexpression elimination, polarity, positive function type, intrinsic types}
}
Document
Artifact
Compiling with Arrays (Artifact)

Authors: David Richter, Timon Böhler, Pascal Weisenburger, and Mira Mezini

Published in: DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)


Abstract
Linear algebra computations are foundational for neural networks and machine learning, often handled through arrays. While many functional programming languages feature lists and recursion, arrays in linear algebra demand constant-time access and bulk operations. To bridge this gap, some languages represent arrays as (eager) functions instead of lists. In this paper, we connect this idea to a formal logical foundation by interpreting functions as the usual negative types from polarized type theory, and arrays as the corresponding dual positive version of the function type. Positive types are defined to have a single elimination form whose computational interpretation is pattern matching. Just like (positive) product types bind two variables during pattern matching, (positive) array types bind variables with multiplicity during pattern matching. We follow a similar approach for Booleans by introducing conditionally-defined variables. The positive formulation for the array type enables us to combine typed partial evaluation and common subexpression elimination into an elegant algorithm whose result enjoys a property we call maximal fission, which we argue can be beneficial for further optimizations. For this purpose, we present the novel intermediate representation indexed administrative normal form (A_{i}NF), which relies on the formal logical foundation of the positive formulation for the array type to facilitate maximal loop fission and subsequent optimizations. A_{i}NF is normal with regard to commuting conversion for both let-bindings and for-loops, leading to flat and maximally fissioned terms. We mechanize the translation and normalization from a simple surface language to A_{i}NF, establishing that the process terminates, preserves types, and produces maximally fissioned terms.

Cite as

David Richter, Timon Böhler, Pascal Weisenburger, and Mira Mezini. Compiling with Arrays (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 18:1-18:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@Article{richter_et_al:DARTS.10.2.18,
  author =	{Richter, David and B\"{o}hler, Timon and Weisenburger, Pascal and Mezini, Mira},
  title =	{{Compiling with Arrays (Artifact)}},
  pages =	{18:1--18:7},
  journal =	{Dagstuhl Artifacts Series},
  ISBN =	{978-3-95977-342-3},
  ISSN =	{2509-8195},
  year =	{2024},
  volume =	{10},
  number =	{2},
  editor =	{Richter, David and B\"{o}hler, Timon and Weisenburger, Pascal and Mezini, Mira},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.18},
  URN =		{urn:nbn:de:0030-drops-209168},
  doi =		{10.4230/DARTS.10.2.18},
  annote =	{Keywords: array languages, functional programming, domain-specific languages, normalization by evaluation, common subexpression elimination, polarity, positive function type, intrinsic types}
}
Document
A Direct-Style Effect Notation for Sequential and Parallel Programs

Authors: David Richter, Timon Böhler, Pascal Weisenburger, and Mira Mezini

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


Abstract
Modeling sequential and parallel composition of effectful computations has been investigated in a variety of languages for a long time. In particular, the popular do-notation provides a lightweight effect embedding for any instance of a monad. Idiom bracket notation, on the other hand, provides an embedding for applicatives. First, while monads force effects to be executed sequentially, ignoring potential for parallelism, applicatives do not support sequential effects. Composing sequential with parallel effects remains an open problem. This is even more of an issue as real programs consist of a combination of both sequential and parallel segments. Second, common notations do not support invoking effects in direct-style, instead forcing a rigid structure upon the code. In this paper, we propose a mixed applicative/monadic notation that retains parallelism where possible, but allows sequentiality where necessary. We leverage a direct-style notation where sequentiality or parallelism is derived from the structure of the code. We provide a mechanisation of our effectful language in Coq and prove that our compilation approach retains the parallelism of the source program.

Cite as

David Richter, Timon Böhler, Pascal Weisenburger, and Mira Mezini. A Direct-Style Effect Notation for Sequential and Parallel Programs. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{richter_et_al:LIPIcs.ECOOP.2023.25,
  author =	{Richter, David and B\"{o}hler, Timon and Weisenburger, Pascal and Mezini, Mira},
  title =	{{A Direct-Style Effect Notation for Sequential and Parallel Programs}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{25:1--25:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.25},
  URN =		{urn:nbn:de:0030-drops-182181},
  doi =		{10.4230/LIPIcs.ECOOP.2023.25},
  annote =	{Keywords: do-notation, parallelism, concurrency, effects}
}
Document
Artifact
A Direct-Style Effect Notation for Sequential and Parallel Programs (Artifact)

Authors: David Richter, Timon Böhler, Pascal Weisenburger, and Mira Mezini

Published in: DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)


Abstract
Modeling sequential and parallel composition of effectful computations has been investigated in a variety of languages for a long time. In particular, the popular do-notation provides a lightweight effect embedding for any instance of a monad. Idiom bracket notation, on the other hand, provides an embedding for applicatives. First, while monads force effects to be executed sequentially, ignoring potential for parallelism, applicatives do not support sequential effects. Composing sequential with parallel effects remains an open problem. This is even more of an issue as real programs consist of a combination of both sequential and parallel segments. Second, common notations do not support invoking effects in direct-style, instead forcing a rigid structure upon the code. In this paper, we propose a mixed applicative/monadic notation that retains parallelism where possible, but allows sequentiality where necessary. We leverage a direct-style notation where sequentiality or parallelism is derived from the structure of the code. We provide a mechanisation of our effectful language in Coq and prove that our compilation approach retains the parallelism of the source program.

Cite as

David Richter, Timon Böhler, Pascal Weisenburger, and Mira Mezini. A Direct-Style Effect Notation for Sequential and Parallel Programs (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 17:1-17:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@Article{richter_et_al:DARTS.9.2.17,
  author =	{Richter, David and B\"{o}hler, Timon and Weisenburger, Pascal and Mezini, Mira},
  title =	{{A Direct-Style Effect Notation for Sequential and Parallel Programs (Artifact)}},
  pages =	{17:1--17:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Richter, David and B\"{o}hler, Timon and Weisenburger, Pascal and Mezini, Mira},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.17},
  URN =		{urn:nbn:de:0030-drops-182573},
  doi =		{10.4230/DARTS.9.2.17},
  annote =	{Keywords: do-notation, parallelism, concurrency, effects}
}
Document
Artifact
Prisma: A Tierless Language for Enforcing Contract-Client Protocols in Decentralized Applications (Artifact)

Authors: David Richter, David Kretzler, Pascal Weisenburger, Guido Salvaneschi, Sebastian Faust, and Mira Mezini

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


Abstract
Decentralized applications (dApps) consist of smart contracts that run on blockchains and clients that model collaborating parties. dApps are used to model financial and legal business functionality. Today, contracts and clients are written as separate programs - in different programming languages - communicating via send and receive operations. This makes distributed program flow awkward to express and reason about, increasing the potential for mismatches in the client-contract interface, which can be exploited by malicious clients, potentially leading to huge financial losses. In this paper, we present Prisma, a language for tierless decentralized applications, where the contract and its clients are defined in one unit. Pairs of send and receive actions that “belong together” are encapsulated into a single direct-style operation, which is executed differently by sending and receiving parties. This enables expressing distributed program flow via standard control flow and renders mismatching communication impossible. We prove formally that our compiler preserves program behavior in presence of an attacker controlling the client code. We systematically compare Prisma with mainstream and advanced programming models for dApps and provide empirical evidence for its expressiveness and performance.

Cite as

David Richter, David Kretzler, Pascal Weisenburger, Guido Salvaneschi, Sebastian Faust, and Mira Mezini. Prisma: A Tierless Language for Enforcing Contract-Client Protocols in Decentralized Applications (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 16:1-16:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@Article{richter_et_al:DARTS.8.2.16,
  author =	{Richter, David and Kretzler, David and Weisenburger, Pascal and Salvaneschi, Guido and Faust, Sebastian and Mezini, Mira},
  title =	{{Prisma: A Tierless Language for Enforcing Contract-Client Protocols in Decentralized Applications (Artifact)}},
  pages =	{16:1--16:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Richter, David and Kretzler, David and Weisenburger, Pascal and Salvaneschi, Guido and Faust, Sebastian and Mezini, Mira},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.16},
  URN =		{urn:nbn:de:0030-drops-162149},
  doi =		{10.4230/DARTS.8.2.16},
  annote =	{Keywords: Domain Specific Languages, Smart Contracts, Scala}
}
Document
Extended Abstract
Prisma: A Tierless Language for Enforcing Contract-Client Protocols in Decentralized Applications (Extended Abstract)

Authors: David Richter, David Kretzler, Pascal Weisenburger, Guido Salvaneschi, Sebastian Faust, and Mira Mezini

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


Abstract
Decentralized applications (dApps) consist of smart contracts that run on blockchains and clients that model collaborating parties. dApps are used to model financial and legal business functionality. Today, contracts and clients are written as separate programs - in different programming languages - communicating via send and receive operations. This makes distributed program flow awkward to express and reason about, increasing the potential for mismatches in the client-contract interface, which can be exploited by malicious clients, potentially leading to huge financial losses. In this paper, we present Prisma, a language for tierless decentralized applications, where the contract and its clients are defined in one unit. Pairs of send and receive actions that "belong together" are encapsulated into a single direct-style operation, which is executed differently by sending and receiving parties. This enables expressing distributed program flow via standard control flow and renders mismatching communication impossible. We prove formally that our compiler preserves program behavior in presence of an attacker controlling the client code. We systematically compare Prisma with mainstream and advanced programming models for dApps and provide empirical evidence for its expressiveness and performance. The design space of dApp programming and other multi-party languages depends on one major choice: a local model versus a global model. In a local model, parties are defined in separate programs and their interactions are encoded via send and receive effects. In a global language, parties are defined within one shared program and interactions are encoded via combined send-and-receive operations with no effects visible to the outside world. The global model is followed by tierless [Christian Queinnec, 2000; Cooper et al., 2007; Choi and Chang, 2019; Fowler et al., 2019; Serrano et al., 2006; Serrano and Prunet, 2016; Radanne et al., 2016; Weisenburger et al., 2018] and choreographic [Kohei Honda et al., 2011; Fabrizio Montesi et al., 2014; Saverio Giallorenzo et al., 2020] languages. However, known approaches to dApp programming follow the local model, thus rely on explicitly specifying the client-contract interaction protocol. Moreover, the contract and clients are implemented in different languages, hence, developers have to master two technology stacks. The dominating approach in industry is Solidity [Mix, 2019] for the contract and JavaScript for clients. Solidity relies on expressing the protocol using assertions in the contract code, which are checked at run time [Solidity documentation - common patterns, 2020]. Failing to insert the correct assertions may give parties illegal access to monetary values to the detriment of others [Nikolić et al., 2018; Luu et al., 2016]. In research, contract languages [Ankush Das et al., 2019; Michael J. Coblenz, 2017; Franklin Schrans et al., 2018; Franklin Schrans et al., 2019; Michael J. Coblenz et al., 2019; Michael J. Coblenz et al., 2019; Reed Oei et al., 2020; Sam Blackshear et al., 2019] have been proposed that rely on advanced type systems such as session types, type states, and linear types. The global model has not been explored for dApp programming. This is unfortunate given the potential to get by with a standard typing discipline and to avoid intricacies and potential mismatches of a two-language stack. Our work fills this gap by proposing Prisma - the first language that features a global programming model for Ethereum dApps. While we focus on the Ethereum blockchain, we believe our techniques to be applicable to other smart contract platforms. Prisma enables interleaving contract and client logic within the same program and adopts a direct style (DS) notation for encoding send-and-receive operations (with our awaitCl language construct) akin to languages with async/await [Gavin M. Bierman et al., 2012; Scala async rfc]. DS addresses shortcomings with the currently dominant encoding of the protocol’s finite state machines (FSM) [Mix, 2019; Michael J. Coblenz, 2017; Franklin Schrans et al., 2018; Franklin Schrans et al., 2019; Michael J. Coblenz et al., 2019; Michael J. Coblenz et al., 2019]. We argue writing FSM style corresponds to a control-flow graph of basic blocks, which is low-level and more suited to be written by a compiler than by a human. With FSM style, the contract is a passive entity whose execution is driven by clients. whereas the DS encoding allows the contract to actively ask clients for input, fitting dApp execution where a dominant contract controls execution and diverts control to other parties when their input is needed. In the following Prisma snippet, the payout function is a function invoked by the contract when it is time to pay money to a client. In Prisma, variables, methods and classes are separated into two namespaces, one for the contract and one for the clients. The payout method is located on the contract via the annotation @co. The body of the method diverts the control to the client using awaitCl(...) { ... }, hence the contained readLine call is executed on the client. Note that no explicit send/receive operations are needed but the communication protocol is expressed through the program control flow. Only after the check client == toBePayed that the correct client replied, the current contact balance balance() is transferred to the client via transfer. @co def payout(toBePayed: Arr[Address]): Unit = { awaitCl(client => client == toBePayed) { readLine("Press enter for payout") } toBePayed.transfer(balance()) } Overall, Prisma relieves the developer from the responsibility of correctly managing distributed, asynchronous program flows and the heterogeneous technology stack. Instead, the burden is put on the compiler, which distributes the program flow by means of selective continuation-passing-style (CPS) translation and defunctionalisation and inserts guards against malicious client interactions. We needed to develop a CPS translation for the code that runs on the Ethereum Virtual Machine (EVM) since the EVM has no built-in support for concurrency primitives which could be used for asynchronous communication. While CPS translations are well-known, we cannot use them out-of-the-box because the control flow is interwoven with distribution in our case. A CPS translation that does not take distribution into account would allow malicious clients to force the contract to deviate from the intended control flow by sending a spoofed continuation. Thus, it was imperative to prove correctness of our distributed CPS translation to ensure control-flow integrity of the contract.

Cite as

David Richter, David Kretzler, Pascal Weisenburger, Guido Salvaneschi, Sebastian Faust, and Mira Mezini. Prisma: A Tierless Language for Enforcing Contract-Client Protocols in Decentralized Applications (Extended Abstract). In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 35:1-35:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{richter_et_al:LIPIcs.ECOOP.2022.35,
  author =	{Richter, David and Kretzler, David and Weisenburger, Pascal and Salvaneschi, Guido and Faust, Sebastian and Mezini, Mira},
  title =	{{Prisma: A Tierless Language for Enforcing Contract-Client Protocols in Decentralized Applications}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{35:1--35:4},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.35},
  URN =		{urn:nbn:de:0030-drops-162632},
  doi =		{10.4230/LIPIcs.ECOOP.2022.35},
  annote =	{Keywords: Domain Specific Languages, Smart Contracts, Scala}
}
Document
Pearl
Multiparty Languages: The Choreographic and Multitier Cases (Pearl)

Authors: Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, David Richter, Guido Salvaneschi, and Pascal Weisenburger

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


Abstract
Choreographic languages aim to express multiparty communication protocols, by providing primitives that make interaction manifest. Multitier languages enable programming computation that spans across several tiers of a distributed system, by supporting primitives that allow computation to change the location of execution. Rooted into different theoretical underpinnings - respectively process calculi and lambda calculus - the two paradigms have been investigated independently by different research communities with little or no contact. As a result, the link between the two paradigms has remained hidden for long. In this paper, we show that choreographic languages and multitier languages are surprisingly similar. We substantiate our claim by isolating the core abstractions that differentiate the two approaches and by providing algorithms that translate one into the other in a straightforward way. We believe that this work paves the way for joint research and cross-fertilisation among the two communities.

Cite as

Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, David Richter, Guido Salvaneschi, and Pascal Weisenburger. Multiparty Languages: The Choreographic and Multitier Cases (Pearl). In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 22:1-22:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{giallorenzo_et_al:LIPIcs.ECOOP.2021.22,
  author =	{Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Richter, David and Salvaneschi, Guido and Weisenburger, Pascal},
  title =	{{Multiparty Languages: The Choreographic and Multitier Cases}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{22:1--22:27},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.22},
  URN =		{urn:nbn:de:0030-drops-140658},
  doi =		{10.4230/LIPIcs.ECOOP.2021.22},
  annote =	{Keywords: Distributed Programming, Choreographies, Multitier Languages}
}
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