Showing 1–2 of 2 results for author: Gopinathan, K
-
GopCaml: A Structural Editor for OCaml
Authors:
Kiran Gopinathan
Abstract:
This talk presents Gopcaml-mode, the first structural editing plugin for OCaml. We will give a tour of the main plugin features, discussing the plugin's internal design and its integration with existing OCaml and GNU Emacs toolchains.
This talk presents Gopcaml-mode, the first structural editing plugin for OCaml. We will give a tour of the main plugin features, discussing the plugin's internal design and its integration with existing OCaml and GNU Emacs toolchains.
△ Less
Submitted 15 July, 2022;
originally announced July 2022.
-
Certifying Certainty and Uncertainty in Approximate Membership Query Structures -- Extended Version
Authors:
Kiran Gopinathan,
Ilya Sergey
Abstract:
Approximate Membership Query structures (AMQs) rely on randomisation for time- and space-efficiency, while introducing a possibility of false positive and false negative answers. Correctness proofs of such structures involve subtle reasoning about bounds on probabilities of getting certain outcomes. Because of these subtleties, a number of unsound arguments in such proofs have been made over the y…
▽ More
Approximate Membership Query structures (AMQs) rely on randomisation for time- and space-efficiency, while introducing a possibility of false positive and false negative answers. Correctness proofs of such structures involve subtle reasoning about bounds on probabilities of getting certain outcomes. Because of these subtleties, a number of unsound arguments in such proofs have been made over the years. In this work, we address the challenge of building rigorous and reusable computer-assisted proofs about probabilistic specifications of AMQs. We describe the framework for systematic decomposition of AMQs and their properties into a series of interfaces and reusable components. We implement our framework as a library in the Coq proof assistant and showcase it by encoding in it a number of non-trivial AMQs, such as Bloom filters, counting filters, quotient filters and blocked constructions, and mechanising the proofs of their probabilistic specifications. We demonstrate how AMQs encoded in our framework guarantee the absence of false negatives by construction. We also show how the proofs about probabilities of false positives for complex AMQs can be obtained by means of verified reduction to the implementations of their simpler counterparts. Finally, we provide a library of domain-specific theorems and tactics that allow a high degree of automation in probabilistic proofs.
△ Less
Submitted 28 April, 2020;
originally announced April 2020.
