| The Lean theorem prover (system description) L de Moura, S Kong, J Avigad, F Van Doorn, J von Raumer Automated Deduction-CADE-25: 25th International Conference on Automated …, 2015 | 462 | 2015 |
| A machine-checked proof of the odd order theorem G Gonthier, A Asperti, J Avigad, Y Bertot, C Cohen, F Garillot, S Le Roux, ... Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013 | 456 | 2013 |
| Gödel’s functional (“Dialectica”) interpretation J Avigad, S Feferman Handbook of proof theory 137, 337-405, 1998 | 316 | 1998 |
| δ-Complete Decision Procedures for Satisfiability over the Reals S Gao, J Avigad, EM Clarke Automated Reasoning: 6th International Joint Conference, IJCAR 2012 …, 2012 | 202 | 2012 |
| A formal system for Euclid’s Elements J Avigad, E Dean, J Mumma The Review of Symbolic Logic 2 (4), 700-768, 2009 | 184 | 2009 |
| A formally verified proof of the prime number theorem J Avigad, K Donnelly, D Gray, P Raff ACM Transactions on Computational Logic (TOCL) 9 (1), 2-es, 2007 | 106 | 2007 |
| Local stability of ergodic averages J Avigad, P Gerhardy, H Towsner Transactions of the American Mathematical Society 362 (1), 261-288, 2010 | 103 | 2010 |
| Formally verified mathematics J Avigad, J Harrison Communications of the ACM 57 (4), 66-75, 2014 | 102 | 2014 |
| A metaprogramming framework for formal verification G Ebner, S Ullrich, J Roesch, J Avigad, L de Moura Proceedings of the ACM on Programming Languages 1 (ICFP), 1-29, 2017 | 91 | 2017 |
| Computability and analysis: the legacy of Alan Turing. J Avigad, V Brattka, R Downey Turing's Legacy, 1-47, 2014 | 91 | 2014 |
| Delta-decidability over the reals S Gao, J Avigad, EM Clarke 2012 27th Annual IEEE Symposium on Logic in Computer Science, 305-314, 2012 | 90 | 2012 |
| Building a push-button RESOLVE verifier: Progress and challenges M Sitaraman, B Adcock, J Avigad, D Bronish, P Bucci, D Frazier, ... Formal Aspects of Computing 23, 607-626, 2011 | 88 | 2011 |
| Mathematical method and proof J Avigad Synthese 153, 105-159, 2006 | 88 | 2006 |
| Number theory and elementary arithmetic J Avigad Philosophia mathematica 11 (3), 257-284, 2003 | 86 | 2003 |
| Understanding proofs J Avigad Carnegie Mellon University, 2008 | 82 | 2008 |
| The epsilon calculus J Avigad, R Zach | 76 | 2002 |
| Methodology and metaphysics in the development of Dedekind's theory of ideals J Avigad Carnegie Mellon University, 2006 | 63 | 2006 |
| Interpreting classical theories in constructive ones J Avigad The Journal of Symbolic Logic 65 (4), 1785-1812, 2000 | 63 | 2000 |
| Formalizing forcing arguments in subsystems of second-order arithmetic J Avigad Annals of Pure and Applied Logic 82 (2), 165-191, 1996 | 59 | 1996 |
| A formally verified proof of the central limit theorem J Avigad, J Hölzl, L Serafin Journal of Automated Reasoning 59 (4), 389-423, 2017 | 44 | 2017 |
Leonardo de MouraSenior Principal Researcher at MicrosoftVerified email at microsoft.com
