5 Search Results for "Rice, Alex A."

Document
DOI: 10.4230/OASIcs.ATMOS.2024.2
Indexing Graphs for Shortest Beer Path Queries

Authors: David Coudert, Andrea D'Ascenzo, and Mattia D'Emidio

Published in: OASIcs, Volume 123, 24th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2024)

Abstract
A beer graph is an edge-weighted graph G = (V,E,ω) with beer vertices B ⊆ V. A beer path between two vertices s and t of a beer graph is a path that connects s and t and visits at least one vertex in B. The beer distance between two vertices is the weight of a shortest beer path, i.e. a beer path having minimum total weight. A graph indexing scheme is a two-phase method that constructs an index data structure by a one-time preprocessing of an input graph and then exploits it to compute (or accelerate the computation of) answers to queries on structures of the graph dataset. In the last decade, such indexing schemes have been designed to perform, effectively, many relevant types of queries, e.g. on reachability, and have gained significant popularity in essentially all data-intensive application domains where large number of queries have to be routinely answered (e.g. journey planners), since they have been shown, through many experimental studies, to offer extremely low query times at the price of limited preprocessing time and space overheads. In this paper, we showcase that an indexing scheme, to efficiently execute queries on beer distances or shortest beer paths for pairs of vertices of a beer graph, can be obtained by adapting the highway labeling, a recently introduced indexing method to accelerate the computation of classical shortest paths. We design a preprocessing algorithm to build a whl index, i.e. a weighted highway labeling of a beer graph, and show how it can be queried to compute beer distances and shortest beer paths. Through extensive experimentation on real networks, we empirically demonstrate its practical effectiveness and superiority, in terms of offered trade-off between preprocessing time, space overhead and query time, with respect to the state-of-the-art.
Cite as

David Coudert, Andrea D'Ascenzo, and Mattia D'Emidio. Indexing Graphs for Shortest Beer Path Queries. In 24th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2024). Open Access Series in Informatics (OASIcs), Volume 123, pp. 2:1-2:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{coudert_et_al:OASIcs.ATMOS.2024.2,
  author =	{Coudert, David and D'Ascenzo, Andrea and D'Emidio, Mattia},
  title =	{{Indexing Graphs for Shortest Beer Path Queries}},
  booktitle =	{24th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2024)},
  pages =	{2:1--2:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-350-8},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{123},
  editor =	{Bouman, Paul C. and Kontogiannis, Spyros C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2024.2},
  URN =		{urn:nbn:de:0030-drops-211907},
  doi =		{10.4230/OASIcs.ATMOS.2024.2},
  annote =	{Keywords: Graph Algorithms, Indexing Schemes, Beer Distances, Algorithms Engineering}
}
Document
DOI: 10.4230/LIPIcs.AFT.2024.20
Optimizing Exit Queues for Proof-Of-Stake Blockchains: A Mechanism Design Approach

Authors: Michael Neuder, Mallesh Pai, and Max Resnick

Published in: LIPIcs, Volume 316, 6th Conference on Advances in Financial Technologies (AFT 2024)

Abstract
Byzantine fault-tolerant consensus protocols have provable safety and liveness properties for static validator sets. In practice, however, the validator set changes over time, potentially eroding the protocol’s security guarantees. For example, systems with accountable safety may lose some of that accountability over time as adversarial validators exit. As a result, protocols must rate limit entry and exit so that the set changes slowly enough to ensure security. Here, the system designer faces a fundamental trade-off. The harder it is to exit the system, the less attractive staking becomes; alternatively, the easier it is to exit the system, the less secure the protocol will be. This paper provides the first systematic study of exit queues for Proof-of-Stake blockchains. Given a collection of validator-set consistency constraints imposed by the protocol, the social planner’s goal is to provide a constrained-optimal mechanism that minimizes disutility for the participants. We introduce the MINSLACK mechanism, a dynamic capacity first-come-first-served queue in which the amount of stake that can exit in a period depends on the number of previous exits and the consistency constraints. We show that MINSLACK is optimal when stakers equally value the processing of their withdrawal. When stakers values are heterogeneous, the optimal mechanism resembles a priority queue with dynamic capacity. However, this mechanism must reserve exit capacity for the future in case a staker with a much higher need for liquidity arrives. We conclude with a survey of known consistency constraints and highlight the diversity of existing exit mechanisms.
Cite as

Michael Neuder, Mallesh Pai, and Max Resnick. Optimizing Exit Queues for Proof-Of-Stake Blockchains: A Mechanism Design Approach. In 6th Conference on Advances in Financial Technologies (AFT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 316, pp. 20:1-20:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{neuder_et_al:LIPIcs.AFT.2024.20,
  author =	{Neuder, Michael and Pai, Mallesh and Resnick, Max},
  title =	{{Optimizing Exit Queues for Proof-Of-Stake Blockchains: A Mechanism Design Approach}},
  booktitle =	{6th Conference on Advances in Financial Technologies (AFT 2024)},
  pages =	{20:1--20:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-345-4},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{316},
  editor =	{B\"{o}hme, Rainer and Kiffer, Lucianna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AFT.2024.20},
  URN =		{urn:nbn:de:0030-drops-209564},
  doi =		{10.4230/LIPIcs.AFT.2024.20},
  annote =	{Keywords: Mechanism Design, Market Design, Accountable Safety, Proof-of-Stake, Blockchain}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.22
Automating Boundary Filling in Cubical Agda

Authors: Maximilian Doré, Evan Cavallo, and Anders Mörtberg

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
When working in a proof assistant, automation is key to discharging routine proof goals such as equations between algebraic expressions. Homotopy Type Theory allows the user to reason about higher structures, such as topological spaces, using higher inductive types (HITs) and univalence. Cubical Agda is an extension of Agda with computational support for HITs and univalence. A difficulty when working in Cubical Agda is dealing with the complex combinatorics of higher structures, an infinite-dimensional generalisation of equational reasoning. To solve these higher-dimensional equations consists in constructing cubes with specified boundaries. We develop a simplified cubical language in which we isolate and study two automation problems: contortion solving, where we attempt to "contort" a cube to fit a given boundary, and the more general Kan solving, where we search for solutions that involve pasting multiple cubes together. Both problems are difficult in the general case - Kan solving is even undecidable - so we focus on heuristics that perform well on practical examples. We provide a solver for the contortion problem using a reformulation of contortions in terms of poset maps, while we solve Kan problems using constraint satisfaction programming. We have implemented our algorithms in an experimental Haskell solver that can be used to automatically solve goals presented by Cubical Agda. We illustrate this with a case study establishing the Eckmann-Hilton theorem using our solver, as well as various benchmarks - providing the ground for further study of proof automation in cubical type theories.
Cite as

Maximilian Doré, Evan Cavallo, and Anders Mörtberg. Automating Boundary Filling in Cubical Agda. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{dore_et_al:LIPIcs.FSCD.2024.22,
  author =	{Dor\'{e}, Maximilian and Cavallo, Evan and M\"{o}rtberg, Anders},
  title =	{{Automating Boundary Filling in Cubical Agda}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{22:1--22:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.22},
  URN =		{urn:nbn:de:0030-drops-203514},
  doi =		{10.4230/LIPIcs.FSCD.2024.22},
  annote =	{Keywords: Cubical Agda, Automated Reasoning, Constraint Satisfaction Programming}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.30
homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories

Authors: Nathan Corbyn, Lukas Heidemann, Nick Hu, Chiara Sarti, Calin Tataru, and Jamie Vicary

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
We present the proof assistant homotopy.io for working with finitely-presented semistrict higher categories. The tool runs in the browser with a point-and-click interface, allowing direct manipulation of proof objects via a graphical representation. We describe the user interface and explain how the tool can be used in practice. We also describe the essential subsystems of the tool, including collapse, contraction, expansion, typechecking, and layout, as well as key implementation details including data structure encoding, memoisation, and rendering. These technical innovations have been essential for achieving good performance in a resource-constrained setting.
Cite as

Nathan Corbyn, Lukas Heidemann, Nick Hu, Chiara Sarti, Calin Tataru, and Jamie Vicary. homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 30:1-30:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{corbyn_et_al:LIPIcs.FSCD.2024.30,
  author =	{Corbyn, Nathan and Heidemann, Lukas and Hu, Nick and Sarti, Chiara and Tataru, Calin and Vicary, Jamie},
  title =	{{homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{30:1--30:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.30},
  URN =		{urn:nbn:de:0030-drops-203594},
  doi =		{10.4230/LIPIcs.FSCD.2024.30},
  annote =	{Keywords: Higher category theory, proof assistant, string diagrams}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.14
New Minimal Linear Inferences in Boolean Logic Independent of Switch and Medial

Authors: Anupam Das and Alex A. Rice

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
A linear inference is a valid inequality of Boolean algebra in which each variable occurs at most once on each side. Equivalently, it is a linear rewrite rule on Boolean terms that constitutes a valid implication. Linear inferences have played a significant role in structural proof theory, in particular in models of substructural logics and in normalisation arguments for deep inference proof systems. Systems of linear logic and, later, deep inference are founded upon two particular linear inferences, switch : x ∧ (y ∨ z) → (x ∧ y) ∨ z, and medial : (w ∧ x) ∨ (y ∧ z) → (w ∨ y) ∧ (x ∨ z). It is well-known that these two are not enough to derive all linear inferences (even modulo all valid linear equations), but beyond this little more is known about the structure of linear inferences in general. In particular despite recurring attention in the literature, the smallest linear inference not derivable under switch and medial ("switch-medial-independent") was not previously known. In this work we leverage recently developed graphical representations of linear formulae to build an implementation that is capable of more efficiently searching for switch-medial-independent inferences. We use it to find two "minimal" 8-variable independent inferences and also prove that no smaller ones exist; in contrast, a previous approach based directly on formulae reached computational limits already at 7 variables. One of these new inferences derives some previously found independent linear inferences. The other exhibits structure seemingly beyond the scope of previous approaches we are aware of; in particular, its existence contradicts a conjecture of Das and Strassburger.
Cite as

Anupam Das and Alex A. Rice. New Minimal Linear Inferences in Boolean Logic Independent of Switch and Medial. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{das_et_al:LIPIcs.FSCD.2021.14,
  author =	{Das, Anupam and Rice, Alex A.},
  title =	{{New Minimal Linear Inferences in Boolean Logic Independent of Switch and Medial}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{14:1--14:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.14},
  URN =		{urn:nbn:de:0030-drops-142525},
  doi =		{10.4230/LIPIcs.FSCD.2021.14},
  annote =	{Keywords: rewriting, linear inference, proof theory, linear logic, implementation}
}
  • Refine by Author
  • 1 Cavallo, Evan
  • 1 Corbyn, Nathan
  • 1 Coudert, David
  • 1 D'Ascenzo, Andrea
  • 1 D'Emidio, Mattia
  • Show More...

  • Refine by Classification
  • 1 Computing methodologies → Theorem proving algorithms
  • 1 Information systems
  • 1 Information systems → Information systems applications
  • 1 Software and its engineering → Software notations and tools
  • 1 Theory of computation → Automated reasoning
  • Show More...

  • Refine by Keyword
  • 1 Accountable Safety
  • 1 Algorithms Engineering
  • 1 Automated Reasoning
  • 1 Beer Distances
  • 1 Blockchain
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 4 2024
  • 1 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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