2 Search Results for "Schubert, Simon"

Document
DOI: 10.4230/LIPIcs.OPODIS.2016.24
Non-Determinism in Byzantine Fault-Tolerant Replication

Authors: Christian Cachin, Simon Schubert, and Marko Vukolic

Published in: LIPIcs, Volume 70, 20th International Conference on Principles of Distributed Systems (OPODIS 2016)

Abstract
Service replication distributes an application over many processes for tolerating faults, attacks, and misbehavior among a subset of the processes. With the recent interest in blockchain technologies, distributed execution of one logical application has become a prominent topic. The established state-machine replication paradigm inherently requires the application to be deterministic. This paper distinguishes three models for dealing with non-determinism in replicated services, where some processes are subject to faults and arbitrary behavior (so-called Byzantine faults): first, the modular case that does not require any changes to the potentially non-deterministic application (and neither access to its internal data); second, master-slave solutions, where ties are broken by a leader and the other processes validate the choices of the leader; and finally, applications that use cryptography and secret keys. Cryptographic operations and secrets must be treated specially because they require strong randomness to satisfy their goals. The paper also introduces two new protocols. First, Protocol Sieve uses the modular approach and filters out non-deterministic operations in an application. It ensures that all correct processes produce the same outputs and that their internal states do not diverge. A second protocol, called Mastercrypt, implements cryptographically secure randomness generation with a verifiable random function and is appropriate for most situations in which cryptographic secrets are involved. All protocols are described in a generic way and do not assume a particular implementation of the underlying consensus primitive.
Cite as

Christian Cachin, Simon Schubert, and Marko Vukolic. Non-Determinism in Byzantine Fault-Tolerant Replication. In 20th International Conference on Principles of Distributed Systems (OPODIS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 70, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{cachin_et_al:LIPIcs.OPODIS.2016.24,
  author =	{Cachin, Christian and Schubert, Simon and Vukolic, Marko},
  title =	{{Non-Determinism in Byzantine Fault-Tolerant Replication}},
  booktitle =	{20th International Conference on Principles of Distributed Systems (OPODIS 2016)},
  pages =	{24:1--24:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-031-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{70},
  editor =	{Fatourou, Panagiota and Jim\'{e}nez, Ernesto and Pedone, Fernando},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2016.24},
  URN =		{urn:nbn:de:0030-drops-70935},
  doi =		{10.4230/LIPIcs.OPODIS.2016.24},
  annote =	{Keywords: Blockchain, atomic broadcast, consensus, distributed cryptography, verifiable random functions}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2013.107
A Model of Type Theory in Cubical Sets

Authors: Marc Bezem, Thierry Coquand, and Simon Huber

Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)

Abstract
We present a model of type theory with dependent product, sum, and identity, in cubical sets. We describe a universe and explain how to transform an equivalence between two types into an equality. We also explain how to model propositional truncation and the circle. While not expressed internally in type theory, the model is expressed in a constructive metalogic. Thus it is a step towards a computational interpretation of Voevodsky's Univalence Axiom.
Cite as

Marc Bezem, Thierry Coquand, and Simon Huber. A Model of Type Theory in Cubical Sets. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 107-128, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{bezem_et_al:LIPIcs.TYPES.2013.107,
  author =	{Bezem, Marc and Coquand, Thierry and Huber, Simon},
  title =	{{A Model of Type Theory in Cubical Sets}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{107--128},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.107},
  URN =		{urn:nbn:de:0030-drops-46284},
  doi =		{10.4230/LIPIcs.TYPES.2013.107},
  annote =	{Keywords: Models of dependent type theory, cubical sets, Univalent Foundations}
}
  • Refine by Author
  • 1 Bezem, Marc
  • 1 Cachin, Christian
  • 1 Coquand, Thierry
  • 1 Huber, Simon
  • 1 Schubert, Simon
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 1 Blockchain
  • 1 Models of dependent type theory
  • 1 Univalent Foundations
  • 1 atomic broadcast
  • 1 consensus
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2014
  • 1 2017

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