8 citations · 9 across the 5 of their papers we have counts for
5 papers
Grammar Repair with Examples and Tree Automata: Extended Version
Yunjeong Lee, Gokul Rajiv, Ilya Sergey
Context-free grammars (CFGs) are the de-facto formalism for declaratively describing concrete syntax for programming languages and generating parsers. One of the major challenges i…
Beluga: Block Synchronization for BFT Consensus Protocols
Tasos Kichidis, Lefteris Kokoris-Kogias, Arun Koshy +4
Modern high-throughput BFT consensus protocols use streamlined push-pull mechanisms to disseminate blocks and keep happy-path performance optimal. Yet state-of-the-art designs lack…
Concurrent Data Structures Made Easy (Extended Version)
Callista Le, Kiran Gopinathan, Koon Wen Lee +2
Design of an efficient thread-safe concurrent data structure is a balancing act between its implementation complexity and performance. Lock-based concurrent data structures, which…
Mechanised Hypersafety Proofs about Structured Data: Extended Version
Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens +2
Arrays are a fundamental abstraction to represent collections of data. It is often possible to exploit structural properties of the data stored in an array (e.g., repetition or spa…
Small Scale Reflection for the Working Lean User
Vladimir Gladshtein, George Pîrlea, Ilya Sergey
We present the design and implementation of the Small Scale Reflection proof methodology and tactic language (a.k.a. SSR) for the Lean 4 proof assistant. Like its Coq predecessor S…