BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verified Software Toolchains: Fiat-Cryptography -  Adam  Chlipala 
 (Massachusetts Institute of Technology)
DTSTART:20220713T123000Z
DTEND:20220713T130000Z
UID:TALK176642@talks.cam.ac.uk
DESCRIPTION:Big-integer modular arithmetic is surprisingly tricky to imple
 ment efficiently in cryptographic software.&nbsp\; Ten years ago\, all suc
 h implementations for elliptic-curve crypto were coded by hand from scratc
 h for each new prime modulus.&nbsp\; Our Fiat Cryptography project showed 
 how to automate that process with a Coq-verified compiler\, which has sinc
 e been adopted for small but important parts of all major web browsers.&nb
 sp\; I will introduce the different techniques: a mix of data-structure ve
 rification\, partial evaluation\, and classic verified-compiler phases.
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR