Követés
Jeremy Avigad
Jeremy Avigad
Professor of Philosophy and Mathematical Sciences, Carnegie Mellon University
E-mail megerősítve itt: cmu.edu - Kezdőlap
Cím
Hivatkozott rá
Hivatkozott rá
Év
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
6392015
A machine-checked proof of the odd order theorem
G Gonthier, A Asperti, J Avigad, Y Bertot, C Cohen, F Garillot, S Le Roux, ...
International conference on interactive theorem proving, 163-179, 2013
4942013
Gödel’s functional (“Dialectica”) interpretation
J Avigad, S Feferman
Studies in Logic and the Foundations of Mathematics 137, 337-405, 1998
3391998
δ-Complete Decision Procedures for Satisfiability over the Reals
S Gao, J Avigad, EM Clarke
International Joint Conference on Automated Reasoning, 286-300, 2012
2252012
A formal system for Euclid’s Elements
J Avigad, E Dean, J Mumma
The Review of Symbolic Logic 2 (4), 700-768, 2009
1892009
Formally verified mathematics
J Avigad, J Harrison
Communications of the ACM 57 (4), 66-75, 2014
1122014
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
1092017
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
1092007
Local stability of ergodic averages
J Avigad, P Gerhardy, H Towsner
Transactions of the American Mathematical Society 362 (1), 261-288, 2010
1062010
Computability and analysis: the legacy of Alan Turing.
J Avigad, V Brattka, R Downey
Turing's Legacy, 1-47, 2014
1022014
Delta-decidability over the reals
S Gao, J Avigad, EM Clarke
2012 27th Annual IEEE Symposium on Logic in Computer Science, 305-314, 2012
952012
Mathematical method and proof
J Avigad
Synthese 153, 105-159, 2006
942006
Understanding proofs
J Avigad
Carnegie Mellon University, 2008
912008
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
882011
Number theory and elementary arithmetic
J Avigad
Philosophia mathematica 11 (3), 257-284, 2003
882003
The epsilon calculus
J Avigad, R Zach
772002
Methodology and metaphysics in the development of Dedekind's theory of ideals
J Avigad
Carnegie Mellon University, 2006
682006
Interpreting classical theories in constructive ones
J Avigad
The Journal of Symbolic Logic 65 (4), 1785-1812, 2000
672000
Formalizing forcing arguments in subsystems of second-order arithmetic
J Avigad
Annals of Pure and Applied Logic 82 (2), 165-191, 1996
611996
Theorem proving in Lean
J Avigad, L De Moura, S Kong
Release 3 (0), 1-4, 2015
542015
A rendszer jelenleg nem tudja elvégezni a műveletet. Próbálkozzon újra később.
Cikkek 1–20