This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- Correct-by-Construction Cryptographic Arithmetic in Coq by Adam Chlipala ABSTRACT Cryptographic systems include big-integer arithmetic routines that have been subjected to heavy optimization, usually by hand in C or assembly code. The code is often rewritten from scratch for each new set of algorithm parameters. My collaborators and I built a tool Fiat Cryptography to automate generation of these routines, without sacrificing performance compared to the best-known C code. As a bonus, we get machine-checked proofs of correctness. The basic approach works within the Coq theorem prover, using a formally verified compiler to specialize formally verified functional programs to parameters. Today our tool is used by a number of open-source projects, including both Chrome and Firefox for producing parts of their TLS implementations. --- SPEAKER - Adam Chlipala Researcher in scaling machine-checked proofs and advanced FP ideas Adam Chlipala has been on the faculty in computer science at MIT since 2011. He did his undergrad at Carnegie Mellon and his PhD at Berkeley, and his research focuses on clean-slate redesign of computer-systems infrastructure, typically taking advantage of machine-checked proofs of functional correctness. Much of his work uses the Coq proof assistant, about which he has written a popular book, "Certified Programming with Dependent Types." He most enjoys finding opportunities for drastic simplification over incumbent abstractions in computer systems, and some favorite tools toward that end are object-capability systems, transactions, proof-carrying code, and high-level languages with whole-program optimizing compilers. Some projects particularly far along the real-world-adoption curve are Fiat Cryptography, for proof-producing generation of low-level cryptographic code, today run by Chrome for most HTTPS connections; and Ur/Web, a production-quality domain-specific language for Web applications. http://adam.chlipala.net/ --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​