B. Parno, J. Howell, C. Gentry, and M. Raykova, Pinocchio, IEEE Symposium on Security and Privacy, SP 2013, pp.238-252, 2013.
DOI : 10.1145/2856449

C. Costello, C. Fournet, J. Howell, M. Kohlweiss, B. Kreuter et al., Geppetto: Versatile Verifiable Computation, 2015 IEEE Symposium on Security and Privacy, 2015.
DOI : 10.1109/SP.2015.23

R. Gennaro, C. Gentry, B. Parno, and M. Raykova, Quadratic Span Programs and Succinct NIZKs without PCPs, EUROCRYPT, 2013.
DOI : 10.1007/978-3-642-38348-9_37
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.231.912

X. Leroy, Formal certification of a compiler back-end or: Programming a compiler with a proof assistant, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

J. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie, A formally-verified C static analyzer, Proceedings of the 42 nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ser. POPL'15, pp.247-259, 2015.
DOI : 10.1145/2775051.2676966
URL : https://hal.archives-ouvertes.fr/hal-01078386

X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, pp.363-446, 2009.
DOI : 10.1007/s10817-009-9155-4
URL : https://hal.archives-ouvertes.fr/inria-00360768

B. Grégoire, L. Théry, and B. Werner, A Computational Approach to Pocklington Certificates in Type Theory, Functional and Logic Programming, 8th International Symposium Proceedings, ser. Lecture Notes in Computer Science, M. Hagiya and P. Wadler, pp.97-113, 2006.
DOI : 10.1007/11737414_8

G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt et al., EasyCrypt: A Tutorial, Lecture Notes in Computer Science, vol.8604, pp.146-166, 2013.
DOI : 10.1007/978-3-642-22792-9_5
URL : https://hal.archives-ouvertes.fr/hal-01114366

G. Gonthier and A. Mahboubi, A small scale reflection extension for the Coq system, Inria, Tech. Rep, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00258384

G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen et al., A Machine-Checked Proof of the Odd Order Theorem, Interactive Theorem Proving -4th International Conference, pp.163-179, 2013.
DOI : 10.1007/978-3-642-39634-2_14
URL : https://hal.archives-ouvertes.fr/hal-00816699

]. G. Danezis, C. Fournet, J. Groth, and M. Kohlweiss, Square Span Programs with Applications to Succinct NIZK Arguments, Cryptology ePrint Archive, vol.718, issue.11, 2014.
DOI : 10.1007/978-3-662-45611-8_28
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.646.5072

B. Braun, A. J. Feldman, Z. Ren, S. Setty, A. J. Blumberg et al., Verifying computations with state, Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles, SOSP '13, 2013.
DOI : 10.1145/2517349.2522733
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.310.7329

R. S. Wahby, S. Setty, Z. Ren, A. J. Blumberg, and M. Walfish, Efficient RAM and Control Flow in Verifiable Outsourced Computation, Proceedings 2015 Network and Distributed System Security Symposium, 2015.
DOI : 10.14722/ndss.2015.23097

E. Ben-sasson, A. Chiesa, D. Genkin, and E. Tromer, Fast reductions from RAMs to delegatable succinct constraint satisfaction problems, Proceedings of the 4th conference on Innovations in Theoretical Computer Science, ITCS '13, 2013.
DOI : 10.1145/2422436.2422481

E. Ben-sasson, A. Chiesa, E. Tromer, and M. Virza, Scalable zero knowledge via cycles of elliptic curves, Proc. of CRYPTO, 2014.

E. Ben-sasson, A. Chiesa, D. Genkin, E. Tromer, and M. Virza, SNARKs for C: Verifying Program Executions Succinctly and in Zero Knowledge, Proc. of CRYPTO, 2013.
DOI : 10.1007/978-3-642-40084-1_6

S. Zahur and D. Evans, Circuit Structures for Improving Efficiency of Security and Privacy Tools, 2013 IEEE Symposium on Security and Privacy, 2013.
DOI : 10.1109/SP.2013.40

I. Damgard, M. Keller, E. Larraia, V. Pastro, P. Scholl et al., Practical Covertly Secure MPC for Dishonest Majority ??? Or: Breaking the SPDZ Limits, Cryptology ePrint Archive, vol.642, 2012.
DOI : 10.1007/978-3-642-40203-6_1

J. B. Almeida, M. Barbosa, G. Barthe, and F. Dupressoir, Certified computer-aided cryptography, Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security, CCS '13, pp.1217-1230, 2013.
DOI : 10.1145/2508859.2516652

J. B. Almeida, M. Barbosa, E. Bangerter, G. Barthe, S. Krenn et al., Full proof cryptography: verifiable compilation of efficient zero-knowledge protocols, the ACM Conference on Computer and Communications Security, CCS'12, pp.488-500, 2012.

A. Pnueli, M. Siegel, and E. Singerman, Translation validation, Proceedings of the 4 th International Conference on Tools and Algorithms for Construction and Analysis of Systems, ser. TACAS '98, pp.151-166, 1998.
DOI : 10.1007/BFb0054170

Y. Chen, C. Hsu, H. Lin, P. Schwabe, M. Tsai et al., Verifying Curve25519 Software, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS '14, pp.299-309, 2014.
DOI : 10.1145/2660267.2660370
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.564.7481

E. Bartzia and P. Strub, A Formal Library for Elliptic Curves in the Coq Proof Assistant, Interactive Theorem Proving -5th International Conference, pp.77-92, 2014.
DOI : 10.1007/978-3-319-08970-6_6
URL : https://hal.archives-ouvertes.fr/hal-01102288

A. W. Appel, Verification of a Cryptographic Primitive, ACM Transactions on Programming Languages and Systems, vol.37, issue.2, p.7, 2015.
DOI : 10.1145/2701415