BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/1655
DTSTAMP:20260108T112202Z
SUMMARY:Verified Programming Frameworks for Authenticated Data Structures
DESCRIPTION:Speaker: Chaitanya Agarwal (Courant Institute of Mathematical S
 ciences\, New York University)\n\nAbstract: \nAuthenticated data structure
 s (ADSs) allow untrusted third parties to carry out operations which produ
 ce proofs that can be used to verify an operation's output. Such data stru
 ctures are challenging to develop and implement correctly. In this talk\, 
 I will talk about programming frameworks that exploit some structural prop
 erties of ADSs to make the task of correctly implementing ADSs easier: (1)
  lambda-auth - a domain-specific extension of the OCaml programming langua
 ge\, that generates correct and secure ADS binaries automatically\; (2) Au
 thentikit - a library version of lambda-auth currently implemented in OCam
 l. I will also talk about recent work by us (https://dl.acm.org/doi/abs/10
 .1145/3719027.3744801) that gives a formal proof of security and correctne
 ss of Authentikit.\nShort Bio:Chaitanya Agarwal (https://culechetoo.github
 .io) is a 3rd year computer science PhD student at the New York University
 \, advised by Joseph Tassarotti. He is broadly interested in programming l
 anguages and formal verification with a particular focus on verification o
 f security applications. In the past\, he has also worked with Thomas Wies
  on abstract-interpretation analysis for recursive\, higher-order programs
 \, and with Shibashis Guha\, on developing statistical-model-checking tech
 niques for Markov Decision Processes (MDPs). Chaitanya obtained his B.Tech
 . from IIIT Delhi.\n
URL:https://www.tcs.tifr.res.in/web/events/1655
DTSTART;TZID=Asia/Kolkata:20260114T110000
DTEND;TZID=Asia/Kolkata:20260114T120000
LOCATION:A-201 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR