default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: Jeremy Avigad
@inproceedings{DBLP:conf/ijcar/Avigad24,
author = {Jeremy Avigad},
editor = {Christoph Benzm{\"{u}}ller and
Marijn J. H. Heule and
Renate A. Schmidt},
title = {Automated Reasoning for Mathematics},
booktitle = {Automated Reasoning - 12th International Joint Conference, {IJCAR}
2024, Nancy, France, July 3-6, 2024, Proceedings, Part {I}},
series = {Lecture Notes in Computer Science},
volume = {14739},
pages = {3--20},
publisher = {Springer},
year = {2024},
url = {https://doi.org/10.1007/978-3-031-63498-7\_1},
doi = {10.1007/978-3-031-63498-7\_1},
timestamp = {Fri, 02 Aug 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/ijcar/Avigad24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/CluneQBA24,
author = {Joshua Clune and
Yicheng Qian and
Alexander Bentkamp and
Jeremy Avigad},
editor = {Yves Bertot and
Temur Kutsia and
Michael Norrish},
title = {Duper: {A} Proof-Producing Superposition Theorem Prover for Dependent
Type Theory},
booktitle = {15th International Conference on Interactive Theorem Proving, {ITP}
2024, September 9-14, 2024, Tbilisi, Georgia},
series = {LIPIcs},
volume = {309},
pages = {10:1--10:20},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2024},
url = {https://doi.org/10.4230/LIPIcs.ITP.2024.10},
doi = {10.4230/LIPICS.ITP.2024.10},
timestamp = {Mon, 02 Sep 2024 16:55:27 +0200},
biburl = {https://dblp.org/rec/conf/itp/CluneQBA24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/rsl/MackerethA23,
author = {Stephen Mackereth and
Jeremy Avigad},
title = {Two-Sorted Frege Arithmetic is not conservative},
journal = {Rev. Symb. Log.},
volume = {16},
number = {4},
pages = {1199--1232},
year = {2023},
url = {https://doi.org/10.1017/s1755020322000156},
doi = {10.1017/S1755020322000156},
timestamp = {Sat, 08 Jun 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/rsl/MackerethA23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tamm/AvigadBBHN23,
author = {Jeremy Avigad and
Seulkee Baek and
Alexander Bentkamp and
Marijn Heule and
Wojciech Nawrocki},
title = {An Impossible Asylum},
journal = {Am. Math. Mon.},
volume = {130},
number = {5},
pages = {446--453},
year = {2023},
url = {https://doi.org/10.1080/00029890.2023.2176668},
doi = {10.1080/00029890.2023.2176668},
timestamp = {Sun, 04 Aug 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tamm/AvigadBBHN23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/CodelAH23,
author = {Cayden R. Codel and
Jeremy Avigad and
Marijn J. H. Heule},
editor = {Alexander Nadel and
Kristin Yvonne Rozier},
title = {Verified Encodings for {SAT} Solvers},
booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2023, Ames, IA, USA,
October 24-27, 2023},
pages = {141--151},
publisher = {{IEEE}},
year = {2023},
url = {https://doi.org/10.34727/2023/isbn.978-3-85448-060-0\_22},
doi = {10.34727/2023/ISBN.978-3-85448-060-0\_22},
timestamp = {Wed, 13 Dec 2023 14:38:51 +0100},
biburl = {https://dblp.org/rec/conf/fmcad/CodelAH23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/AvigadGLST23,
author = {Jeremy Avigad and
Lior Goldberg and
David Levit and
Yoav Seginer and
Alon Titelman},
editor = {Adam Naumowicz and
Ren{\'{e}} Thiemann},
title = {A Proof-Producing Compiler for Blockchain Applications},
booktitle = {14th International Conference on Interactive Theorem Proving, {ITP}
2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
series = {LIPIcs},
volume = {268},
pages = {7:1--7:19},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2023},
url = {https://doi.org/10.4230/LIPIcs.ITP.2023.7},
doi = {10.4230/LIPICS.ITP.2023.7},
timestamp = {Wed, 21 Aug 2024 22:46:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/AvigadGLST23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sat/BryantNAH23,
author = {Randal E. Bryant and
Wojciech Nawrocki and
Jeremy Avigad and
Marijn J. H. Heule},
editor = {Meena Mahajan and
Friedrich Slivovsky},
title = {Certified Knowledge Compilation with Application to Verified Model
Counting},
booktitle = {26th International Conference on Theory and Applications of Satisfiability
Testing, {SAT} 2023, July 4-8, 2023, Alghero, Italy},
series = {LIPIcs},
volume = {271},
pages = {6:1--6:20},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2023},
url = {https://doi.org/10.4230/LIPIcs.SAT.2023.6},
doi = {10.4230/LIPICS.SAT.2023.6},
timestamp = {Wed, 21 Aug 2024 22:46:00 +0200},
biburl = {https://dblp.org/rec/conf/sat/BryantNAH23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/BentkampMA23,
author = {Alexander Bentkamp and
Ramon Fern{\'{a}}ndez Mir and
Jeremy Avigad},
editor = {Sriram Sankaranarayanan and
Natasha Sharygina},
title = {Verified reductions for optimization},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 29th International Conference, {TACAS} 2023, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2022, Paris, France, April 22-27, 2023, Proceedings, Part {II}},
series = {Lecture Notes in Computer Science},
volume = {13994},
pages = {74--92},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-30820-8\_8},
doi = {10.1007/978-3-031-30820-8\_8},
timestamp = {Sat, 13 May 2023 01:07:18 +0200},
biburl = {https://dblp.org/rec/conf/tacas/BentkampMA23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2301-09347,
author = {Alexander Bentkamp and
Ramon Fern{\'{a}}ndez Mir and
Jeremy Avigad},
title = {Verified reductions for optimization},
journal = {CoRR},
volume = {abs/2301.09347},
year = {2023},
url = {https://doi.org/10.48550/arXiv.2301.09347},
doi = {10.48550/ARXIV.2301.09347},
eprinttype = {arXiv},
eprint = {2301.09347},
timestamp = {Thu, 26 Jan 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2301-09347.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2302-12433,
author = {Zhangir Azerbayev and
Bartosz Piotrowski and
Hailey Schoelkopf and
Edward W. Ayers and
Dragomir Radev and
Jeremy Avigad},
title = {ProofNet: Autoformalizing and Formally Proving Undergraduate-Level
Mathematics},
journal = {CoRR},
volume = {abs/2302.12433},
year = {2023},
url = {https://doi.org/10.48550/arXiv.2302.12433},
doi = {10.48550/ARXIV.2302.12433},
eprinttype = {arXiv},
eprint = {2302.12433},
timestamp = {Tue, 28 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2302-12433.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/AvigadGLST22,
author = {Jeremy Avigad and
Lior Goldberg and
David Levit and
Yoav Seginer and
Alon Titelman},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {A verified algebraic representation of cairo program execution},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {153--165},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503675},
doi = {10.1145/3497775.3503675},
timestamp = {Mon, 05 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/AvigadGLST22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/synthese/Avigad21,
author = {Jeremy Avigad},
title = {Reliability of mathematical inference},
journal = {Synth.},
volume = {198},
number = {8},
pages = {7377--7399},
year = {2021},
url = {https://doi.org/10.1007/s11229-019-02524-y},
doi = {10.1007/S11229-019-02524-Y},
timestamp = {Thu, 16 Sep 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/synthese/Avigad21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/BentkampA21,
author = {Alexander Bentkamp and
Jeremy Avigad},
editor = {Jasmin Blanchette and
James H. Davenport and
Peter Koepke and
Michael Kohlhase and
Andrea Kohlhase and
Adam Naumowicz and
Dennis M{\"{u}}ller and
Yasmine Sharoda and
Claudio Sacerdoti Coen},
title = {Verified Optimization (work in progress)},
booktitle = {Joint Proceedings of the FMM, FVPS, MathUI,NatFoM, and OpenMath Workshops,
Doctoral Program, and Work in Progress at the Conference on Intelligent
Computer Mathematics 2021 co-located with the 14th Conference on Intelligent
Computer Mathematics {(CICM} 2021), Virtual Event, Timisoara, Romania,
July 26 - 31, 2021},
series = {{CEUR} Workshop Proceedings},
volume = {3377},
publisher = {CEUR-WS.org},
year = {2021},
url = {https://ceur-ws.org/Vol-3377/fmm7.pdf},
timestamp = {Thu, 14 Sep 2023 09:27:13 +0200},
biburl = {https://dblp.org/rec/conf/mkm/BentkampA21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2109-14534,
author = {Jeremy Avigad and
Lior Goldberg and
David Levit and
Yoav Seginer and
Alon Titelman},
title = {A verified algebraic representation of Cairo program execution},
journal = {CoRR},
volume = {abs/2109.14534},
year = {2021},
url = {https://arxiv.org/abs/2109.14534},
eprinttype = {arXiv},
eprint = {2109.14534},
timestamp = {Mon, 04 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2109-14534.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2111-06807,
author = {Alexander Bentkamp and
Jeremy Avigad},
title = {Verified Optimization},
journal = {CoRR},
volume = {abs/2111.06807},
year = {2021},
url = {https://arxiv.org/abs/2111.06807},
eprinttype = {arXiv},
eprint = {2111.06807},
timestamp = {Tue, 16 Nov 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2111-06807.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2112-02142,
author = {Jeremy Avigad and
Seulkee Baek and
Alexander Bentkamp and
Marijn Heule and
Wojciech Nawrocki},
title = {An Impossible Asylum},
journal = {CoRR},
volume = {abs/2112.02142},
year = {2021},
url = {https://arxiv.org/abs/2112.02142},
eprinttype = {arXiv},
eprint = {2112.02142},
timestamp = {Wed, 08 Dec 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2112-02142.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/AvigadM20,
author = {Jeremy Avigad and
Assia Mahboubi},
title = {Preface: Selected Extended Papers from Interactive Theorem Proving
2018},
journal = {J. Autom. Reason.},
volume = {64},
number = {5},
pages = {793--794},
year = {2020},
url = {https://doi.org/10.1007/s10817-020-09557-w},
doi = {10.1007/S10817-020-09557-W},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/AvigadM20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/rsl/Avigad20,
author = {Jeremy Avigad},
title = {Modularity in Mathematics},
journal = {Rev. Symb. Log.},
volume = {13},
number = {1},
pages = {47--79},
year = {2020},
url = {https://doi.org/10.1017/S1755020317000387},
doi = {10.1017/S1755020317000387},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/rsl/Avigad20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2008-04262,
author = {Jeremy Avigad and
Floris van Doorn},
title = {Progress on a perimeter surveillance problem},
journal = {CoRR},
volume = {abs/2008.04262},
year = {2020},
url = {https://arxiv.org/abs/2008.04262},
eprinttype = {arXiv},
eprint = {2008.04262},
timestamp = {Mon, 17 Aug 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2008-04262.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2009-09541,
author = {Jeremy Avigad},
title = {Foundations},
journal = {CoRR},
volume = {abs/2009.09541},
year = {2020},
url = {https://arxiv.org/abs/2009.09541},
eprinttype = {arXiv},
eprint = {2009.09541},
timestamp = {Wed, 23 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2009-09541.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/AvigadCH19,
author = {Jeremy Avigad and
Mario Carneiro and
Simon Hudon},
editor = {John Harrison and
John O'Leary and
Andrew Tolmach},
title = {Data Types as Quotients of Polynomial Functors},
booktitle = {10th International Conference on Interactive Theorem Proving, {ITP}
2019, September 9-12, 2019, Portland, OR, {USA}},
series = {LIPIcs},
volume = {141},
pages = {6:1--6:19},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2019},
url = {https://doi.org/10.4230/LIPIcs.ITP.2019.6},
doi = {10.4230/LIPICS.ITP.2019.6},
timestamp = {Wed, 21 Aug 2024 22:46:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/AvigadCH19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lics/AckermanAF0R19,
author = {Nathanael L. Ackerman and
Jeremy Avigad and
Cameron E. Freer and
Daniel M. Roy and
Jason M. Rute},
title = {Algorithmic barriers to representing conditional independence},
booktitle = {34th Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS}
2019, Vancouver, BC, Canada, June 24-27, 2019},
pages = {1--13},
publisher = {{IEEE}},
year = {2019},
url = {https://doi.org/10.1109/LICS.2019.8785762},
doi = {10.1109/LICS.2019.8785762},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lics/AckermanAF0R19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/AvigadBKPPS18,
author = {Jeremy Avigad and
Jasmin Christian Blanchette and
Gerwin Klein and
Lawrence C. Paulson and
Andrei Popescu and
Gregor Snelting},
title = {Introduction to Milestones in Interactive Theorem Proving},
journal = {J. Autom. Reason.},
volume = {61},
number = {1-4},
pages = {1--8},
year = {2018},
url = {https://doi.org/10.1007/s10817-018-9465-5},
doi = {10.1007/S10817-018-9465-5},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/AvigadBKPPS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/AvigadM18,
author = {Jeremy Avigad and
Assia Mahboubi},
editor = {Jeremy Avigad and
Assia Mahboubi},
title = {Erratum to: Interactive Theorem Proving},
booktitle = {Interactive Theorem Proving - 9th International Conference, {ITP}
2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
UK, July 9-12, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10895},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-94821-8\_38},
doi = {10.1007/978-3-319-94821-8\_38},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/AvigadM18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/itp/2018,
editor = {Jeremy Avigad and
Assia Mahboubi},
title = {Interactive Theorem Proving - 9th International Conference, {ITP}
2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
UK, July 9-12, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10895},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-94821-8},
doi = {10.1007/978-3-319-94821-8},
isbn = {978-3-319-94820-1},
timestamp = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/2018.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1801-10387,
author = {Nathanael L. Ackerman and
Jeremy Avigad and
Cameron E. Freer and
Daniel M. Roy and
Jason M. Rute},
title = {On the computability of graphons},
journal = {CoRR},
volume = {abs/1801.10387},
year = {2018},
url = {http://arxiv.org/abs/1801.10387},
eprinttype = {arXiv},
eprint = {1801.10387},
timestamp = {Tue, 04 Jun 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1801-10387.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/AvigadHS17,
author = {Jeremy Avigad and
Johannes H{\"{o}}lzl and
Luke Serafin},
title = {A Formally Verified Proof of the Central Limit Theorem},
journal = {J. Autom. Reason.},
volume = {59},
number = {4},
pages = {389--423},
year = {2017},
url = {https://doi.org/10.1007/s10817-017-9404-x},
doi = {10.1007/S10817-017-9404-X},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/AvigadHS17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/pacmpl/EbnerURAM17,
author = {Gabriel Ebner and
Sebastian Ullrich and
Jared Roesch and
Jeremy Avigad and
Leonardo de Moura},
title = {A metaprogramming framework for formal verification},
journal = {Proc. {ACM} Program. Lang.},
volume = {1},
number = {{ICFP}},
pages = {34:1--34:29},
year = {2017},
url = {https://doi.org/10.1145/3110278},
doi = {10.1145/3110278},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/pacmpl/EbnerURAM17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/AvigadLR16,
author = {Jeremy Avigad and
Robert Y. Lewis and
Cody Roux},
title = {A Heuristic Prover for Real Inequalities},
journal = {J. Autom. Reason.},
volume = {56},
number = {3},
pages = {367--386},
year = {2016},
url = {https://doi.org/10.1007/s10817-015-9356-y},
doi = {10.1007/S10817-015-9356-Y},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/AvigadLR16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/rsl/AvigadM16,
author = {Jeremy Avigad and
Rebecca Lea Morris},
title = {Character and Object},
journal = {Rev. Symb. Log.},
volume = {9},
number = {3},
pages = {480--510},
year = {2016},
url = {https://doi.org/10.1017/S1755020315000398},
doi = {10.1017/S1755020315000398},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/rsl/AvigadM16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cpp/2016,
editor = {Jeremy Avigad and
Adam Chlipala},
title = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
publisher = {{ACM}},
year = {2016},
url = {http://dl.acm.org/citation.cfm?id=2854065},
isbn = {978-1-4503-4127-1},
timestamp = {Mon, 18 Jan 2016 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/2016.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/mscs/AvigadKL15,
author = {Jeremy Avigad and
Krzysztof Kapulkin and
Peter LeFanu Lumsdaine},
title = {Homotopy limits in type theory},
journal = {Math. Struct. Comput. Sci.},
volume = {25},
number = {5},
pages = {1040--1070},
year = {2015},
url = {https://doi.org/10.1017/S0960129514000498},
doi = {10.1017/S0960129514000498},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/mscs/AvigadKL15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/MouraKADR15,
author = {Leonardo Mendon{\c{c}}a de Moura and
Soonho Kong and
Jeremy Avigad and
Floris van Doorn and
Jakob von Raumer},
editor = {Amy P. Felty and
Aart Middeldorp},
title = {The Lean Theorem Prover (System Description)},
booktitle = {Automated Deduction - {CADE-25} - 25th International Conference on
Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9195},
pages = {378--388},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-319-21401-6\_26},
doi = {10.1007/978-3-319-21401-6\_26},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/MouraKADR15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/MouraAKR15,
author = {Leonardo Mendon{\c{c}}a de Moura and
Jeremy Avigad and
Soonho Kong and
Cody Roux},
title = {Elaboration in Dependent Type Theory},
journal = {CoRR},
volume = {abs/1505.04324},
year = {2015},
url = {http://arxiv.org/abs/1505.04324},
eprinttype = {arXiv},
eprint = {1505.04324},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/MouraAKR15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/bsl/Avigad14,
author = {Jeremy Avigad},
title = {Thomas Hales. Dense Sphere Packings: {A} Blueprint for Formal Proofs.
Cambridge University Press, Cambridge, 2012, xiv + 271 pp},
journal = {Bull. Symb. Log.},
volume = {20},
number = {4},
pages = {500--501},
year = {2014},
url = {https://doi.org/10.1017/bsl.2014.35},
doi = {10.1017/BSL.2014.35},
timestamp = {Fri, 03 Jul 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/bsl/Avigad14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/cacm/AvigadH14,
author = {Jeremy Avigad and
John Harrison},
title = {Formally verified mathematics},
journal = {Commun. {ACM}},
volume = {57},
number = {4},
pages = {66--75},
year = {2014},
url = {https://doi.org/10.1145/2591012},
doi = {10.1145/2591012},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/cacm/AvigadH14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/AvigadLR14,
author = {Jeremy Avigad and
Robert Y. Lewis and
Cody Roux},
editor = {Gerwin Klein and
Ruben Gamboa},
title = {A Heuristic Prover for Real Inequalities},
booktitle = {Interactive Theorem Proving - 5th International Conference, {ITP}
2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
Austria, July 14-17, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8558},
pages = {61--76},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-08970-6\_5},
doi = {10.1007/978-3-319-08970-6\_5},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/AvigadLR14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:books/cu/p/AvigadB14,
author = {Jeremy Avigad and
Vasco Brattka},
editor = {Rod Downey},
title = {Computability and analysis: the legacy of Alan Turing},
booktitle = {Turing's Legacy: Developments from Turing's Ideas in Logic},
series = {Lecture Notes in Logic},
volume = {42},
pages = {1--47},
publisher = {Cambridge University Press},
year = {2014},
url = {https://doi.org/10.1017/CBO9781107338579.002},
doi = {10.1017/CBO9781107338579.002},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/books/cu/p/AvigadB14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/AvigadLR14,
author = {Jeremy Avigad and
Robert Y. Lewis and
Cody Roux},
title = {A heuristic prover for real inequalities},
journal = {CoRR},
volume = {abs/1404.4410},
year = {2014},
url = {http://arxiv.org/abs/1404.4410},
eprinttype = {arXiv},
eprint = {1404.4410},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/AvigadLR14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/AvigadHS14,
author = {Jeremy Avigad and
Johannes H{\"{o}}lzl and
Luke Serafin},
title = {A formally verified proof of the Central Limit Theorem},
journal = {CoRR},
volume = {abs/1405.7012},
year = {2014},
url = {http://arxiv.org/abs/1405.7012},
eprinttype = {arXiv},
eprint = {1405.7012},
timestamp = {Sat, 23 Jan 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/AvigadHS14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsyml/Avigad13,
author = {Jeremy Avigad},
title = {Uniform distribution and algorithmic randomness},
journal = {J. Symb. Log.},
volume = {78},
number = {1},
pages = {334--344},
year = {2013},
url = {https://doi.org/10.2178/jsl.7801230},
doi = {10.2178/JSL.7801230},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jsyml/Avigad13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/GonthierAABCGRMOBPRSTT13,
author = {Georges Gonthier and
Andrea Asperti and
Jeremy Avigad and
Yves Bertot and
Cyril Cohen and
Fran{\c{c}}ois Garillot and
St{\'{e}}phane Le Roux and
Assia Mahboubi and
Russell O'Connor and
Sidi Ould Biha and
Ioana Pasca and
Laurence Rideau and
Alexey Solovyev and
Enrico Tassi and
Laurent Th{\'{e}}ry},
editor = {Sandrine Blazy and
Christine Paulin{-}Mohring and
David Pichardie},
title = {A Machine-Checked Proof of the Odd Order Theorem},
booktitle = {Interactive Theorem Proving - 4th International Conference, {ITP}
2013, Rennes, France, July 22-26, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7998},
pages = {163--179},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-39634-2\_14},
doi = {10.1007/978-3-642-39634-2\_14},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/GonthierAABCGRMOBPRSTT13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1304-0680,
author = {Jeremy Avigad and
Krzysztof Kapulkin and
Peter LeFanu Lumsdaine},
title = {Homotopy limits in Coq},
journal = {CoRR},
volume = {abs/1304.0680},
year = {2013},
url = {http://arxiv.org/abs/1304.0680},
eprinttype = {arXiv},
eprint = {1304.0680},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1304-0680.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/AvigadH12,
author = {Jeremy Avigad and
Stefan Hetzl},
title = {Bondy's Theorem},
journal = {Arch. Formal Proofs},
volume = {2012},
year = {2012},
url = {https://www.isa-afp.org/entries/Bondy.shtml},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/AvigadH12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/apal/AvigadDR12,
author = {Jeremy Avigad and
Edward T. Dean and
Jason M. Rute},
title = {Algorithmic randomness, reverse mathematics, and the dominated convergence
theorem},
journal = {Ann. Pure Appl. Log.},
volume = {163},
number = {12},
pages = {1854--1864},
year = {2012},
url = {https://doi.org/10.1016/j.apal.2012.05.010},
doi = {10.1016/J.APAL.2012.05.010},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/apal/AvigadDR12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/eatcs/Avigad12,
author = {Jeremy Avigad},
title = {Type Inference in Mathematics},
journal = {Bull. {EATCS}},
volume = {106},
pages = {78--98},
year = {2012},
url = {http://eatcs.org/beatcs/index.php/beatcs/article/view/81},
timestamp = {Fri, 12 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/eatcs/Avigad12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jla/AvigadDR12,
author = {Jeremy Avigad and
Edward T. Dean and
Jason M. Rute},
title = {A metastable dominated convergence theorem},
journal = {J. Log. Anal.},
volume = {4},
year = {2012},
url = {http://logicandanalysis.org/index.php/jla/article/view/138/50},
timestamp = {Fri, 06 Mar 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/jla/AvigadDR12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/ndjfl/Avigad12,
author = {Jeremy Avigad},
title = {Uncomputably Noisy Ergodic Limits},
journal = {Notre Dame J. Formal Log.},
volume = {53},
number = {3},
pages = {347--350},
year = {2012},
url = {https://doi.org/10.1215/00294527-1716757},
doi = {10.1215/00294527-1716757},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/ndjfl/Avigad12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/GaoAC12,
author = {Sicun Gao and
Jeremy Avigad and
Edmund M. Clarke},
editor = {Bernhard Gramlich and
Dale Miller and
Uli Sattler},
title = {{\(\delta\)}-Complete Decision Procedures for Satisfiability over
the Reals},
booktitle = {Automated Reasoning - 6th International Joint Conference, {IJCAR}
2012, Manchester, UK, June 26-29, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7364},
pages = {286--300},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-31365-3\_23},
doi = {10.1007/978-3-642-31365-3\_23},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/GaoAC12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lics/GaoAC12,
author = {Sicun Gao and
Jeremy Avigad and
Edmund M. Clarke},
title = {Delta-Decidability over the Reals},
booktitle = {Proceedings of the 27th Annual {IEEE} Symposium on Logic in Computer
Science, {LICS} 2012, Dubrovnik, Croatia, June 25-28, 2012},
pages = {305--314},
publisher = {{IEEE} Computer Society},
year = {2012},
url = {https://doi.org/10.1109/LICS.2012.41},
doi = {10.1109/LICS.2012.41},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lics/GaoAC12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1204-3513,
author = {Sicun Gao and
Jeremy Avigad and
Edmund M. Clarke},
title = {Delta-Complete Decision Procedures for Satisfiability over the Reals},
journal = {CoRR},
volume = {abs/1204.3513},
year = {2012},
url = {http://arxiv.org/abs/1204.3513},
eprinttype = {arXiv},
eprint = {1204.3513},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1204-3513.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1204-6671,
author = {Sicun Gao and
Jeremy Avigad and
Edmund M. Clarke},
title = {Delta-Decidability over the Reals},
journal = {CoRR},
volume = {abs/1204.6671},
year = {2012},
url = {http://arxiv.org/abs/1204.6671},
eprinttype = {arXiv},
eprint = {1204.6671},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1204-6671.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1206-3431,
author = {Jeremy Avigad and
Vasco Brattka},
title = {Computability and analysis: the legacy of Alan Turing},
journal = {CoRR},
volume = {abs/1206.3431},
year = {2012},
url = {http://arxiv.org/abs/1206.3431},
eprinttype = {arXiv},
eprint = {1206.3431},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1206-3431.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fac/SitaramanAABBFFHHKKSW11,
author = {Murali Sitaraman and
Bruce M. Adcock and
Jeremy Avigad and
Derek Bronish and
Paolo Bucci and
David Frazier and
Harvey M. Friedman and
Heather K. Harton and
Wayne D. Heym and
Jason Kirschenbaum and
Joan Krone and
Hampton Smith and
Bruce W. Weide},
title = {Building a push-button {RESOLVE} verifier: Progress and challenges},
journal = {Formal Aspects Comput.},
volume = {23},
number = {5},
pages = {607--626},
year = {2011},
url = {https://doi.org/10.1007/s00165-010-0154-3},
doi = {10.1007/S00165-010-0154-3},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/fac/SitaramanAABBFFHHKKSW11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/mscs/AspertiA11,
author = {Andrea Asperti and
Jeremy Avigad},
title = {Zen and the art of formalisation},
journal = {Math. Struct. Comput. Sci.},
volume = {21},
number = {4},
pages = {679--682},
year = {2011},
url = {https://doi.org/10.1017/S0960129511000065},
doi = {10.1017/S0960129511000065},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/mscs/AspertiA11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1111-5885,
author = {Jeremy Avigad},
title = {Type inference in mathematics},
journal = {CoRR},
volume = {abs/1111.5885},
year = {2011},
url = {http://arxiv.org/abs/1111.5885},
eprinttype = {arXiv},
eprint = {1111.5885},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1111-5885.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tplp/Avigad10,
author = {Jeremy Avigad},
title = {\emph{Handbook of Practical Logic and Automated Reasoning}, John Harrison,
Cambridge University Press, 2009. Hardcover, {ISBN-13:} 978-0-521-89957-4,
681 pp. + xix, {\textdollar}135.00},
journal = {Theory Pract. Log. Program.},
volume = {10},
number = {2},
pages = {237--241},
year = {2010},
url = {https://doi.org/10.1017/S1471068410000037},
doi = {10.1017/S1471068410000037},
timestamp = {Thu, 13 Feb 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tplp/Avigad10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/apal/Avigad09,
author = {Jeremy Avigad},
title = {The metamathematics of ergodic theory},
journal = {Ann. Pure Appl. Log.},
volume = {157},
number = {2-3},
pages = {64--76},
year = {2009},
url = {https://doi.org/10.1016/j.apal.2008.09.001},
doi = {10.1016/J.APAL.2008.09.001},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/apal/Avigad09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsyml/AvigadT09,
author = {Jeremy Avigad and
Henry Towsner},
title = {Functional interpretation and inductive definitions},
journal = {J. Symb. Log.},
volume = {74},
number = {4},
pages = {1100--1120},
year = {2009},
url = {https://doi.org/10.2178/jsl/1254748682},
doi = {10.2178/JSL/1254748682},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jsyml/AvigadT09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/rsl/AvigadDM09,
author = {Jeremy Avigad and
Edward T. Dean and
John Mumma},
title = {A Formal System for Euclid's Elements},
journal = {Rev. Symb. Log.},
volume = {2},
number = {4},
pages = {700--768},
year = {2009},
url = {https://doi.org/10.1017/S1755020309990098},
doi = {10.1017/S1755020309990098},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/rsl/AvigadDM09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-0805-1386,
author = {Steven Kieffer and
Jeremy Avigad and
Harvey Friedman},
title = {A language for mathematical language management},
journal = {CoRR},
volume = {abs/0805.1386},
year = {2008},
url = {http://arxiv.org/abs/0805.1386},
eprinttype = {arXiv},
eprint = {0805.1386},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-0805-1386.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/AvigadD07,
author = {Jeremy Avigad and
Kevin Donnelly},
title = {A Decision Procedure for Linear "Big O" Equations},
journal = {J. Autom. Reason.},
volume = {38},
number = {4},
pages = {353--373},
year = {2007},
url = {https://doi.org/10.1007/s10817-007-9066-1},
doi = {10.1007/S10817-007-9066-1},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/AvigadD07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tcs/AvigadY07,
author = {Jeremy Avigad and
Yimu Yin},
title = {Quantifier elimination for the reals with a predicate for the powers
of two},
journal = {Theor. Comput. Sci.},
volume = {370},
number = {1-3},
pages = {48--59},
year = {2007},
url = {https://doi.org/10.1016/j.tcs.2006.10.005},
doi = {10.1016/J.TCS.2006.10.005},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tcs/AvigadY07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tocl/AvigadDGR07,
author = {Jeremy Avigad and
Kevin Donnelly and
David Gray and
Paul Raff},
title = {A formally verified proof of the prime number theorem},
journal = {{ACM} Trans. Comput. Log.},
volume = {9},
number = {1},
pages = {2},
year = {2007},
url = {https://doi.org/10.1145/1297658.1297660},
doi = {10.1145/1297658.1297660},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tocl/AvigadDGR07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-cs-0701073,
author = {Jeremy Avigad and
Kevin Donnelly},
title = {A decision procedure for linear "big O" equations},
journal = {CoRR},
volume = {abs/cs/0701073},
year = {2007},
url = {http://arxiv.org/abs/cs/0701073},
eprinttype = {arXiv},
eprint = {cs/0701073},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-cs-0701073.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/apal/AvigadS06,
author = {Jeremy Avigad and
Ksenija Simic},
title = {Fundamental notions of analysis in subsystems of second-order arithmetic},
journal = {Ann. Pure Appl. Log.},
volume = {139},
number = {1-3},
pages = {138--184},
year = {2006},
url = {https://doi.org/10.1016/j.apal.2005.03.004},
doi = {10.1016/J.APAL.2005.03.004},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/apal/AvigadS06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/lmcs/AvigadF06,
author = {Jeremy Avigad and
Harvey Friedman},
title = {Combining decision procedures for the reals},
journal = {Log. Methods Comput. Sci.},
volume = {2},
number = {4},
year = {2006},
url = {https://doi.org/10.2168/LMCS-2(4:4)2006},
doi = {10.2168/LMCS-2(4:4)2006},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/lmcs/AvigadF06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/synthese/Avigad06,
author = {Jeremy Avigad},
title = {Mathematical Method and Proof},
journal = {Synth.},
volume = {153},
number = {1},
pages = {105--159},
year = {2006},
url = {https://doi.org/10.1007/s11229-005-4064-5},
doi = {10.1007/S11229-005-4064-5},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/synthese/Avigad06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-cs-0601134,
author = {Jeremy Avigad and
Harvey Friedman},
title = {Combining decision procedures for the reals},
journal = {CoRR},
volume = {abs/cs/0601134},
year = {2006},
url = {http://arxiv.org/abs/cs/0601134},
eprinttype = {arXiv},
eprint = {cs/0601134},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-cs-0601134.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-cs-0610117,
author = {Jeremy Avigad and
Yimu Yin},
title = {Quantifier elimination for the reals with a predicate for the powers
of two},
journal = {CoRR},
volume = {abs/cs/0610117},
year = {2006},
url = {http://arxiv.org/abs/cs/0610117},
eprinttype = {arXiv},
eprint = {cs/0610117},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-cs-0610117.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/apal/BeckmannAM05,
author = {Arnold Beckmann and
Jeremy Avigad and
Georg Moser},
title = {Preface},
journal = {Ann. Pure Appl. Log.},
volume = {136},
number = {1-2},
pages = {1--2},
year = {2005},
url = {https://doi.org/10.1016/j.apal.2005.05.001},
doi = {10.1016/J.APAL.2005.05.001},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/apal/BeckmannAM05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-cs-0509025,
author = {Jeremy Avigad and
Kevin Donnelly and
David Gray and
Paul Raff},
title = {A formally verified proof of the prime number theorem},
journal = {CoRR},
volume = {abs/cs/0509025},
year = {2005},
url = {http://arxiv.org/abs/cs/0509025},
eprinttype = {arXiv},
eprint = {cs/0509025},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-cs-0509025.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/bsl/Avigad04,
author = {Jeremy Avigad},
title = {Forcing in proof theory},
journal = {Bull. Symb. Log.},
volume = {10},
number = {3},
pages = {305--333},
year = {2004},
url = {https://doi.org/10.2178/bsl/1102022660},
doi = {10.2178/BSL/1102022660},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/bsl/Avigad04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/AvigadD04,
author = {Jeremy Avigad and
Kevin Donnelly},
editor = {David A. Basin and
Micha{\"{e}}l Rusinowitch},
title = {Formalizing {O} Notation in Isabelle/HOL},
booktitle = {Automated Reasoning - Second International Joint Conference, {IJCAR}
2004, Cork, Ireland, July 4-8, 2004, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3097},
pages = {357--371},
publisher = {Springer},
year = {2004},
url = {https://doi.org/10.1007/978-3-540-25984-8\_27},
doi = {10.1007/978-3-540-25984-8\_27},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/AvigadD04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/apal/Avigad03,
author = {Jeremy Avigad},
title = {Erratum to "Saturated models of universal theories": [Ann.
Pure Appl. Logic 118 {(2002)} 219-234]},
journal = {Ann. Pure Appl. Log.},
volume = {121},
number = {2-3},
pages = {285},
year = {2003},
url = {https://doi.org/10.1016/S0168-0072(03)00004-6},
doi = {10.1016/S0168-0072(03)00004-6},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/apal/Avigad03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tocl/Avigad03,
author = {Jeremy Avigad},
title = {Eliminating definitions and Skolem functions in first-order logic},
journal = {{ACM} Trans. Comput. Log.},
volume = {4},
number = {3},
pages = {402--415},
year = {2003},
url = {https://doi.org/10.1145/772062.772068},
doi = {10.1145/772062.772068},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tocl/Avigad03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/aml/AvigadH02,
author = {Jeremy Avigad and
Jeremy Helzner},
title = {Transfer principles in nonstandard intuitionistic arithmetic},
journal = {Arch. Math. Log.},
volume = {41},
number = {6},
pages = {581--602},
year = {2002},
url = {https://doi.org/10.1007/s001530100109},
doi = {10.1007/S001530100109},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/aml/AvigadH02.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/apal/Avigad02,
author = {Jeremy Avigad},
title = {Saturated models of universal theories},
journal = {Ann. Pure Appl. Log.},
volume = {118},
number = {3},
pages = {219--234},
year = {2002},
url = {https://doi.org/10.1016/S0168-0072(02)00030-1},
doi = {10.1016/S0168-0072(02)00030-1},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/apal/Avigad02.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jml/Avigad02,
author = {Jeremy Avigad},
title = {An Ordinal Analysis of Admissible Set Theory using Recursion on Ordinal
Notations},
journal = {J. Math. Log.},
volume = {2},
number = {1},
year = {2002},
url = {https://doi.org/10.1142/S0219061302000126},
doi = {10.1142/S0219061302000126},
timestamp = {Fri, 18 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jml/Avigad02.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/mlq/Avigad02,
author = {Jeremy Avigad},
title = {Update Procedures and the 1-Consistency of Arithmetic},
journal = {Math. Log. Q.},
volume = {48},
number = {1},
pages = {3--13},
year = {2002},
url = {https://doi.org/10.1002/1521-3870(200201)48:1\&\#60;3::AID-MALQ3\&\#62;3.0.CO;2-6},
doi = {10.1002/1521-3870(200201)48:1\&\#60;3::AID-MALQ3\&\#62;3.0.CO;2-6},
timestamp = {Wed, 17 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/mlq/Avigad02.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jlp/Avigad01,
author = {Jeremy Avigad},
title = {Algebraic proofs of cut elimination},
journal = {J. Log. Algebraic Methods Program.},
volume = {49},
number = {1-2},
pages = {15--30},
year = {2001},
url = {https://doi.org/10.1016/S1567-8326(01)00009-1},
doi = {10.1016/S1567-8326(01)00009-1},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jlp/Avigad01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/sigact/Avigad01,
author = {Jeremy Avigad},
title = {Review of "Basic proof theory: second edition" by A. S.
Troelstra and H. Schwichtenberg. Cambridge University Press},
journal = {{SIGACT} News},
volume = {32},
number = {2},
pages = {15--19},
year = {2001},
url = {https://doi.org/10.1145/504192.1005766},
doi = {10.1145/504192.1005766},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/sigact/Avigad01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lics/Avigad01,
author = {Jeremy Avigad},
title = {Eliminating Definitions and Skolem Functions in First-Order Logic},
booktitle = {16th Annual {IEEE} Symposium on Logic in Computer Science, Boston,
Massachusetts, USA, June 16-19, 2001, Proceedings},
pages = {139--146},
publisher = {{IEEE} Computer Society},
year = {2001},
url = {https://doi.org/10.1109/LICS.2001.932490},
doi = {10.1109/LICS.2001.932490},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lics/Avigad01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsyml/Avigad00,
author = {Jeremy Avigad},
title = {Interpreting Classical Theories in Constructive Ones},
journal = {J. Symb. Log.},
volume = {65},
number = {4},
pages = {1785--1812},
year = {2000},
url = {https://doi.org/10.2307/2695075},
doi = {10.2307/2695075},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jsyml/Avigad00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsyml/AvigadS99,
author = {Jeremy Avigad and
Richard Sommer},
title = {The Model-Theoretic Ordinal Analysis of Theories of Predicative Strength},
journal = {J. Symb. Log.},
volume = {64},
number = {1},
pages = {327--349},
year = {1999},
url = {https://doi.org/10.2307/2586768},
doi = {10.2307/2586768},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jsyml/AvigadS99.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/aml/Avigad98,
author = {Jeremy Avigad},
title = {An effective proof that open sets are Ramsey},
journal = {Arch. Math. Log.},
volume = {37},
number = {4},
pages = {235--240},
year = {1998},
url = {https://doi.org/10.1007/s001530050095},
doi = {10.1007/S001530050095},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/aml/Avigad98.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/apal/Avigad98,
author = {Jeremy Avigad},
title = {Predicative Functionals and an Interpretation of ID\({}_{\mbox{{\textless}omega}}\)},
journal = {Ann. Pure Appl. Log.},
volume = {92},
number = {1},
pages = {1--34},
year = {1998},
url = {https://doi.org/10.1016/S0168-0072(97)00045-6},
doi = {10.1016/S0168-0072(97)00045-6},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/apal/Avigad98.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/bsl/AvigadS97,
author = {Jeremy Avigad and
Richard Sommer},
title = {A model-theoretic approach to ordinal analysis},
journal = {Bull. Symb. Log.},
volume = {3},
number = {1},
pages = {17--52},
year = {1997},
url = {https://doi.org/10.2307/421195},
doi = {10.2307/421195},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/bsl/AvigadS97.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/apal/Avigad96,
author = {Jeremy Avigad},
title = {Formalizing Forcing Arguments in Subsystems of Second-Order Arithmetic},
journal = {Ann. Pure Appl. Log.},
volume = {82},
number = {2},
pages = {165--191},
year = {1996},
url = {https://doi.org/10.1016/0168-0072(96)00003-6},
doi = {10.1016/0168-0072(96)00003-6},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/apal/Avigad96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsyml/Avigad96,
author = {Jeremy Avigad},
title = {On the Relationship Between ATR\({}_{\mbox{0}}\) and ID\({}_{\mbox{{\textless}omega}}\)},
journal = {J. Symb. Log.},
volume = {61},
number = {3},
pages = {768--779},
year = {1996},
url = {https://doi.org/10.2307/2275783},
doi = {10.2307/2275783},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jsyml/Avigad96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/dimacs/Avigad96,
author = {Jeremy Avigad},
editor = {Paul Beame and
Samuel R. Buss},
title = {Plausibly hard combinatorial tautologies},
booktitle = {Proof Complexity and Feasible Arithmetics, Proceedings of a {DIMACS}
Workshop, New Brunswick, New Jersey, USA, April 21-24, 1996},
series = {{DIMACS} Series in Discrete Mathematics and Theoretical Computer Science},
volume = {39},
pages = {1--12},
publisher = {{DIMACS/AMS}},
year = {1996},
url = {https://doi.org/10.1090/dimacs/039/01},
doi = {10.1090/DIMACS/039/01},
timestamp = {Sat, 30 Sep 2023 09:38:58 +0200},
biburl = {https://dblp.org/rec/conf/dimacs/Avigad96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-09-04 01:22 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
