Distributed Consensus, Revisited

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

We propose a new approach for normalization and simplification of logical formulas. Our approach is based on algorithms for lattice-like structures. Specifically, we present two efficient algorithms for computing a normal form and deciding the word problem ...

Type-level programming is becoming more and more popular in the realm of functional programming. However, the combination of type-level programming and subtyping remains largely unexplored in practical programming languages. This paper presents match types ...

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

Many programming languages in the OO tradition now support pattern matching in some form. Historical examples include Scala and Ceylon, with the more recent additions of Java, Kotlin, TypeScript, and Flow. But pattern matching on generic class hierarchies ...

Two prominent categories for achieving coordinated multirobot displacement are flocking and navigation in formation. Both categories have their own body of literature and characteristics, including their respective advantages and disadvantages. While typic ...

Formally verifying the correctness of software network functions (NFs) is necessary for network reliability, yet existing techniques require full source code and mandate the use of specific data structures. We describe an automated technique to verify NF b ...

Over the past decade, the Scala community has shown great interest in using type-level programming to obtain additional type safety. Unfortunately, the lack of support from the Scala compiler has been a barrier to the adoption of that technique, notably du ...

The fabrication of high-hardness non-hydrogenated diamond-like carbon (DLC) via standard magnetron sputtering (MS) is often hindered by the low sputtering yields and ionisation rates of carbon, therefore investigations into pulsed alternatives of MS, else ...

We present a quasilinear time algorithm to decide the word problem on a natural algebraic structures we call orthocomplemented bisemilattices, a subtheory of boolean algebra. We use as a base a variation of Hopcroft, Ullman and Aho algorithm for tree isomo ...

Advances in mobile computing have paved the way for new types of distributed applications that can be executed solely by mobile devices on Device-to-Device (D2D) ecosystems (e.g., crowdsensing). Sophisticated applications, like cryptocurrencies, need distr ...

We show that a constant factor approximation of the shortest and closest lattice vector problem in any l(p)-norm can be computed in time 2((0.802 + epsilon)n). This matches the currently fastest constant factor approximation algorithm for the shortest vect ...

It's been a little more than 40 years since researchers first suggested exploiting quantum physics to build more powerful computers. During this time, we have seen the development of many quantum algorithms and significant technological advances to make th ...

Distributed Consensus, Revisited

Chat with Graph Search

Formula Normalizations in Verification

Type-Level Programming with Match Types

Scaling Language Features for Program Verification

A case for DOT: Theoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning

Hybrid Flock - Formation Control Algorithms

Automated Verification of Network Function Binaries

Abstractions for Type-Level Programming

From pulsed-DCMS and HiPIMS to microwave plasma-assisted sputtering: Their influence on the properties of diamond-like carbon films

Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time

Toward Mobile Distributed Ledgers

Approximate CVPp in time 2(0.802n)

Practical Compilation of Quantum Programs