BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//CERN//INDICO//EN
BEGIN:VEVENT
SUMMARY:Most Models are Query Models
DTSTART:20260529T103000Z
DTEND:20260529T123000Z
DTSTAMP:20260618T121900Z
UID:indico-event-9351@scitalks.tifr.res.in
DESCRIPTION:Speakers: Shreyas Srinivas (CISPA\, Germany)\n\nAbstract: Int
 eractive theorem proving has matured to the point where substantial mathem
 atical results can be verified in systems such as Lean. In theoretical com
 puter science\, however\, formalization remains difficult outside areas wi
 th well-developed tools\, such as programming languages\, distributed syst
 ems\, and cryptology. In particular\, there is no unified Lean library for
  algorithmic theory comparable in scope to mathlib. A bottom-up approach t
 o such a library would require formalizing low-level compu­ tational mode
 ls\, such as RAM models\, and then rebuilding decades of algorithmic theor
 y 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. \nHowever there might be a simpler path. A recurring feat
 ure of algorithmic theory is that algorithms are rarely presented as low-l
 evel executable programs. They are instead built from existing procedures\
 , data-structure operations\, and model-specific primitives. Given these p
 rimitives and their costs\, the complexity of an algorithm is usually anal
 yzed compositionally. More complex primitives can in turn be expressed in 
 terms of simpler ones\, suggesting a modular hierarchy of algorithmic mode
 ls that can eventually be related to basic models. \nThis talk presents a
  lightweight lean framework for formalizing such arguments\, which I call 
 the query- combinator model. The central idea is to treat opaque computati
 onal primitives as queries\, equipped with models describing its behavior 
 and cost. Algorithms are built by combining queries\, using free monads. C
 omplexity bounds can then be proved structurally from the costs of the que
 ries an algorithm performs\, without first constructing a full low-level m
 odel such as a RAM machine. We show that this framework covers traditional
  sequential algorithms and also extends to models ranging from the Roberts
 on-Webb model for fair cake cutting to classical and quantum circuits. Our
  end-goal is to isolate the relevant combinatorial arguments of an algorit
 hm from implementation details. \nThis work builds on several strands of 
 existing literature: lightweight monadic verification of algo­ rithmic co
 mplexity\, free monads\, and formalized query or oracle models from crypto
 logy. Existing approaches tend to target particular models or classes of a
 lgorithms. To the best of our knowledge\, this is the first framework to c
 ombine these ideas into a unified approach for formalizing a broad range o
 f algorithmic models and reductions between them.\nAbout Speaker:Shreyas S
 rinivas is a final-year PhD student at the CISPA Helmholtz Center for Info
 rmation Security\, advised by Prof. Christoph Lenzen\, currently at Reykja
 vik University. His work spans distributed clock synchronization\, ASIC de
 sign for clocking in VLSI systems\, and formalization in Lean. He was a ma
 intainer of the Equational Theories Project\, and with his co-authors refu
 ted the conjecture thatEFX allocations always exist for monotone valuation
  functions in discrete fair division. His current research focuses on inte
 grating interactive theorem provers into theoretical computer science.\n\n
 https://scitalks.tifr.res.in/event/9351/
LOCATION:Speaker will join via ZOOM (AG-66\, TIFR\, Mumbai)
URL:https://scitalks.tifr.res.in/event/9351/
END:VEVENT
END:VCALENDAR