BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/1762
DTSTAMP:20260825T045150Z
SUMMARY:Designing formally proven Hardware: A rocq+clash based approach.
DESCRIPTION:Speaker: Piyush Kurur (IIT Palakkad)\n\nAbstract: \nA certified
  programming project in rocq (like CompCert for example) develops the pro
 gram together with its proof of correctness in rocq. Actual executable so
 ftware is then obtained by first extracting to Haskell (or Ocaml or Schem
 e) followed by compiling with the the Haskell compiler. The machine check
 ed proofs that are part of the original rocq source acts as quality assur
 ance certificates of the executable.\nThe Clash project is a Haskell to Ha
 rdware (VHDL or Verilog) compiler so with the extraction mechanism one ca
 n use a similar approach for hardware as well. However\, due to the natur
 e of Hardware this is not so straight forward. In this talk\, I will show
  how to use the above outlined approach to get high assurance\, high perf
 ormance hardware. Our main contribution is a rocq library for building c
 ertified regular expression matcher in hardware. I will start by explaini
 ng the basics of interactive theorem proving in rocq and themechanism for 
 developing certified programs. We will look at some of the challenges tha
 t needs to be addressed in order to get hardware out of such programs.Thi
 s is joint work with Julin Shaji and Sandeep Chandran. The associated cod
 e is available from the public repository.https://gitlab.com/piyush-kurur/
 regexp-hardware\nBrief bio: Ph.D\, Institute of Mathematical Science then 
 faculty at IIT Kanpur and currently at IIT Palakkad.\n
URL:https://www.tcs.tifr.res.in/web/events/1762
DTSTART;TZID=Asia/Kolkata:20260915T160000
DTEND;TZID=Asia/Kolkata:20260915T170000
LOCATION:A-201 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR