Simple High-Level Code For Cryptographic Arithmetic With Proofs, Without Compromises

Simple High-Level Code For Cryptographic Arithmetic With Proofs, Without Compromises

Show other versions (1)

We introduce an unusual approach for implementing cryptographic arithmetic in short high-level code with machinechecked proofs of functional correctness. We further demonstrate that simple partial evaluation is sufficient to transform such initial code into highly competitive C code, breaking the de...

Full description

Bibliographic Details
Main Authors: Erbsen, Andres, Philipoom, Jade D., Gross, Jason S., Sloan, Robert Hal, Chlipala, Adam
Other Authors: Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory
Format: Article
Language:English
Published: Association for Computing Machinery (ACM) 2021
Online Access:https://hdl.handle.net/1721.1/131080

Internet

https://hdl.handle.net/1721.1/131080

Similar Items