nLab Jason Gross

• MO user page

• webpage

Selected writings

On internal categories in homotopy type theory:

• Jason Gross, Adam Chlipala, David Spivak, Experience Implementing a Performant Category-Theory Library in Coq, In: Interactive Theorem Proving. ITP 2014 Lecture Notes in Computer Science, 8558 Springer (2014) $[$arXiv:1401.7694, doi:10.1007/978-3-319-08970-6_18$]$

On cryptography:

• Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala, Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises, 2019 IEEE Symposium on Security and Privacy (SP) $[$doi:10.1109/SP.2019.00005$]$

category: people