An extensible framework for synthesizing efficient, verified parsers by Gross, Jason S

Get full text

Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac by Gross, Jason, Erbsen, Andres, Chlipala, Adam

Get full text

Experience Implementing a Performant Category-Theory Library in Coq by Chlipala, Adam, Spivak, David I., Gross, Jason S.

Get full text
Get full text
Get full text

Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq by Gross, Jason, Erbsen, Andres, Philipoom, Jade, Agrawal, Rajashree, Chlipala, Adam

Get full text

Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant by Delaware, Benjamin James, Pit-Claudel, Clément, Gross, Jason S., Chlipala, Adam

Get full text
Get full text
Get full text
Get full text

Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs by Pit-Claudel, Clément, Wang, Peng, Delaware, Benjamin, Gross, Jason S., Chlipala, Adam

Get full text

Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant by Delaware, Benjamin James, Pit-Claudel, Clement F., Gross, Jason S., Chlipala, Adam

Get full text
Get full text
Get full text
Get full text

Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises by Erbsen, Andres, Philipoom, Jade D., Gross, Jason S., Sloan, Robert Hal, Chlipala, Adam

Get full text

Simple High-Level Code For Cryptographic Arithmetic With Proofs, Without Compromises by Erbsen, Andres, Philipoom, Jade D., Gross, Jason S., Sloan, Robert Hal, Chlipala, Adam

Get full text

Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs by Pit-Claudel, Clement Francois, Wang, Peng, Delaware, Benjamin, Gross, Jason S., Chlipala, Adam

Get full text

The end of history? Using a proof assistant to replace language design with library design by Chlipala, Adam, Delaware, Benjamin, Duchovni, Samuel, Gross, Jason S., Pit-Claudel, Clément, Suriyakarn, Sorawit, Wang, Peng

Get full text

The end of history? Using a proof assistant to replace language design with library design by Chlipala, Adam, Delaware, Benjamin, Duchovni, Samuel, Gross, Jason S., Pit-Claudel, Clement Francois, Suriyakarn, Sorawit, Wang, Peng

Get full text

Evaluation of a field kit for testing arsenic in paddy soil contaminated by irrigation water by Huhmann, Linden B, Harvey, Charles F, Gross, Jason, Uddin, Anjal, Choudhury, Imtiaz, Ahmed, Kazi M, Duxbury, John M, Bostick, Benjamin, van Geen, Alexander

Get full text

Evaluation of a field kit for testing arsenic in paddy soil contaminated by irrigation water by Huhmann, Linden B., Harvey, Charles F., Gross, Jason, Uddin, Anjal, Choudhury, Imtiaz, Ahmed, Kazi M., Duxbury, John M., Bostick, Benjamin, van Geen, Alexander

Get full text

CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives by Kuepper, Joel, Erbsen, Andres, Gross, Jason, Conoly, Owen, Sun, Chuyue, Tian, Samuel, Wu, David, Chlipala, Adam, Chuengsatiansup, Chitchanok, Genkin, Daniel, Wagner, Markus, Yarom, Yuval

Get full text