nLab Adam Chlipala

• webpage

Selected writings

On software verification via dependent type theory with Coq:

• Adam Chlipala, Implementing Certified Programming Language Tools in Dependent Type Theory, Berkeley (2007) [UCB/EECS-2007-113, pdf, web]

• Adam Chlipala, Certified programming with dependent types, MIT Press 2013 (ISBN:9780262026659, pdf, book webpage)

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