Choose timezone
Your profile timezone:
Powered by Indico
v3.3.3
Abstract:
Interactive theorem proving has matured to the point where substantial mathematical results can be verified in systems such as Lean. In theoretical computer science, however, formalization remains difficult outside areas with well-developed tools, such as programming languages, distributed systems, and cryptology. In particular, there is no unified Lean library for algorithmic theory comparable in scope to mathlib. A bottom-up approach to such a library would require formalizing low-level compu tational models, such as RAM models, and then rebuilding decades of algorithmic theory on top of them. This is further complicated by the variety of models and prolixity of algorithms in the literature. Thus such an undertaking would be formidable.
However there might be a simpler path. A recurring feature of algorithmic theory is that algorithms are rarely presented as low-level executable programs. They are instead built from existing procedures, data-structure operations, and model-specific primitives. Given these primitives and their costs, the complexity of an algorithm is usually analyzed compositionally. More complex primitives can in turn be expressed in terms of simpler ones, suggesting a modular hierarchy of algorithmic models that can eventually be related to basic models.
This talk presents a lightweight lean framework for formalizing such arguments, which I call the query- combinator model. The central idea is to treat opaque computational primitives as queries, equipped with models describing its behavior and cost. Algorithms are built by combining queries, using free monads. Complexity bounds can then be proved structurally from the costs of the queries an algorithm performs, without first constructing a full low-level model such as a RAM machine. We show that this framework covers traditional sequential algorithms and also extends to models ranging from the Robertson-Webb model for fair cake cutting to classical and quantum circuits. Our end-goal is to isolate the relevant combinatorial arguments of an algorithm from implementation details.
This work builds on several strands of existing literature: lightweight monadic verification of algo rithmic complexity, free monads, and formalized query or oracle models from cryptology. Existing approaches tend to target particular models or classes of algorithms. To the best of our knowledge, this is the first framework to combine these ideas into a unified approach for formalizing a broad range of algorithmic models and reductions between them.
About Speaker:
Shreyas Srinivas is a final-year PhD student at the CISPA Helmholtz Center for Information Security, advised by Prof. Christoph Lenzen, currently at Reykjavik University. His work spans distributed clock synchronization, ASIC design for clocking in VLSI systems, and formalization in Lean. He was a maintainer of the Equational Theories Project, and with his co-authors refuted the conjecture that
EFX allocations always exist for monotone valuation functions in discrete fair division. His current research focuses on integrating interactive theorem provers into theoretical computer science.