Blum, M. Program result checking: A new approach to making programs more reliable. In Proceedings of the 20^th International Colloquium on Automata, Languages and Programming (Lund, Sweden, July 5--9), A. Lingas, R. Karlsson, and S. Carlsson, Eds. Springer, Berlin, 1993, 1--14.

Digital Library

Google Scholar

[3]

Bourbaki, N. Elements of Mathematics: Theory of Sets. Addison-Wesley, Reading, MA, 1968; translated from the French Théorie des ensembles in the series Eléments de mathématique, revised version, Hermann, Paris, 1970.

Google Scholar

[4]

Gödel, K. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik 38, 1 (1931), 173--198; reprinted with English translation in Kurt Gödel: Collected Works, Volume 1, S. Feferman et al., Eds. Oxford University Press, Oxford, U.K., 1986, 144--195.

Google Scholar

[5]

Gonthier, G. Formal proof---The four-color theorem. Notices of the American Mathematical Society 55, 11 (Dec. 2008), 1382--1393.

Google Scholar

[6]

Grabiner, J.V. Is mathematical truth time-dependent? In New Directions in the Philosophy of Mathematics: An Anthology, T. Tymoczko, Ed., Birkhäuser, Boston, 1986, 201--213.

Google Scholar

[7]

Grcar, J.F. Errors and corrections in the mathematical literature. Notices of the American Mathematical Society 60, 4 (Apr. 2013), 418--432.

Crossref

Google Scholar

[8]

Hales, T. Dense Sphere Packings: A Blueprint for Formal Proofs. Cambridge University Press, Cambridge, U.K., 2012.

Digital Library

Google Scholar

[9]

Hales, T. The Kepler Conjecture (unpublished manuscript), 1998; http://arxiv.org/pdf/math/9811078.pdf

Google Scholar

[10]

Harrison, J. Towards self-verification of HOL Light. In Proceedings of the Third International Joint Conference in Automated Reasoning (Seattle, Aug. 17--20), U. Furbach and N. Shankar, Eds. Springer, Berlin, 2006, 177--191.

Digital Library

Google Scholar

[11]

Harrison, J. and Théry, L. A sceptic's approach to combining HOL and Maple. Journal of Automated Reasoning 21, 3 (1998), 279--294.

Digital Library

Google Scholar

[12]

Hobbes, T. Leviathan. Andrew Crooke, London, 1651.

Google Scholar

[13]

Jaffe, A. and Quinn, F. 'Theoretical mathematics': Toward a cultural synthesis of mathematics and theoretical physics. Bulletin of the American Mathematics Society (New Series) 29, 1 (1993), 1--13.

Google Scholar

[14]

Littlewood, J.E. Littlewood's Miscellany. Cambridge University Press, Cambridge, U.K., 1986.

Google Scholar

[15]

Mac Lane, S. Mathematics: Form and Function. Springer, New York, 1986.

Google Scholar

[16]

MacKenzie, D. Mechanizing Proof: Computing, Risk and Trust. MIT Press, Cambridge, MA, 2001.

Digital Library

Google Scholar

[17]

McCune, W. Solution of the Robbins problem. Journal of Automated Reasoning 19, 3 (1997), 263--276.

Digital Library

Google Scholar

[18]

Nathanson, M. Desperately seeking mathematical truth. Notices of the American Mathematical Society 55, 7 (Aug. 2008), 773.

Google Scholar

[19]

Nipkow, T., Bauer, G., and Schultz, P. Flyspeck I: Tame graphs. In Proceedings of the Third International Joint Conference in Automated Reasoning (Seattle, Aug. 17--20). Springer, Berlin, 2006, 21--35.

Digital Library

Google Scholar

[20]

Parrilo, P.A. Semidefinite programming relaxations for semialgebraic problems. Mathematical Programming 96, 2 (2003), 293--320.

Crossref

Google Scholar

[21]

Schubring, G. Zur Modernisierung des Studiums der Mathematik in Berlin, 1820--1840. In Amphora: Festschrift für Hans Wussing Zu Seinem 65. Geburtstag, S.S.Demidov et al., Eds. Birkhäuser, Basel, 1992, 649--675.

Google Scholar

[22]

Solovyev, A. Formal Computation and Methods. Ph.D. thesis, University of Pittsburgh, Pittsburgh, PA, 2012.

Digital Library

Google Scholar

[23]

Thurston, W.P. On proof and progress in mathematics. Bulletin of the American Mathematical Society (New Series) 30, 2 (1994), 161--177.

Google Scholar

[24]

Univalent Foundations Program, Institute for Advanced Study. Homotopy Type Theory: Univalent Foundations of Mathematics. Princeton, NJ, 2013; https://github.com/HoTT/book

Google Scholar

[25]

Wiedijk, F. The de Bruijn Factor (unpublished manuscript), 2000; http://www.cs.ru.nl/~freek/factor/

Google Scholar

[26]

Wiedijk, F. The Seventeen Provers of the World. Springer, Berlin, 2006.

Digital Library

Google Scholar

Cited By

View all

Avigad J(2024)Mathematics and the formal turnBulletin of the American Mathematical Society10.1090/bull/183261:2(225-240)Online publication date: 15-Feb-2024
https://doi.org/10.1090/bull/1832
Bobbin MSharlin SFeyzishendi PDang AWraback CJosephson T(2024)Formalizing chemical physics using the Lean theorem proverDigital Discovery10.1039/D3DD00077J3:2(264-280)Online publication date: 2024
https://doi.org/10.1039/D3DD00077J
Prieto-Cubides JGylterud H(2024)On planarity of graphs in homotopy type theoryMathematical Structures in Computer Science10.1017/S0960129524000100(1-41)Online publication date: 8-May-2024
https://doi.org/10.1017/S0960129524000100
Show More Cited By

Recommendations

A Formally Verified NAT
SIGCOMM '17: Proceedings of the Conference of the ACM Special Interest Group on Data Communication

We present a Network Address Translator (NAT) written in C and proven to be semantically correct according to RFC 3022, as well as crash-free and memory-safe. There exists a lot of recent work on network verification, but it mostly assumes models of ...
A Formally Verified Sorting Certifier

In this paper, we describe the use of the certification-trail technique as the basis of a hybrid framework for building formally verified software systems. Our technique involves formally verifying only a part of a software system; however, the ...
Code optimizations using formally verified properties
OOPSLA '13: Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications

Formal program verification offers strong assurance of correctness, backed by the strength of mathematical proof. Constructing these proofs requires humans to identify program invariants, and show that they are always maintained. These invariants are ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Communications of the ACM Volume 57, Issue 4

April 2014

97 pages

ISSN:0001-0782

EISSN:1557-7317

DOI:10.1145/2580723

Editor:
Moshe Y. Vardi
Association for Computing Machinery, New York, NY

Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 April 2014

Published in CACM Volume 57, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article
Popular
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

47
Total Citations
View Citations
29,774
Total Downloads

Downloads (Last 12 months)972
Downloads (Last 6 weeks)42

Reflects downloads up to 28 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Avigad J(2024)Mathematics and the formal turnBulletin of the American Mathematical Society10.1090/bull/183261:2(225-240)Online publication date: 15-Feb-2024
https://doi.org/10.1090/bull/1832
Bobbin MSharlin SFeyzishendi PDang AWraback CJosephson T(2024)Formalizing chemical physics using the Lean theorem proverDigital Discovery10.1039/D3DD00077J3:2(264-280)Online publication date: 2024
https://doi.org/10.1039/D3DD00077J
Prieto-Cubides JGylterud H(2024)On planarity of graphs in homotopy type theoryMathematical Structures in Computer Science10.1017/S0960129524000100(1-41)Online publication date: 8-May-2024
https://doi.org/10.1017/S0960129524000100
Dou GChen SYu WZhang R(2024)The Continuum Hypothesis Implies the Existence of Non-principal Arithmetical Ultrafilters – A Coq Formal VerificationFormal Methods and Software Engineering10.1007/978-981-96-0617-7_15(257-277)Online publication date: 2-Dec-2024
https://dl.acm.org/doi/10.1007/978-981-96-0617-7_15
Macbeth D(2024)Formal Proofs in Mathematical PracticeHandbook of the History and Philosophy of Mathematical Practice10.1007/978-3-031-40846-5_35(2113-2135)Online publication date: 27-Apr-2024
https://doi.org/10.1007/978-3-031-40846-5_35
Andersen L(2024)The Social Epistemology of Mathematical ProofHandbook of the History and Philosophy of Mathematical Practice10.1007/978-3-031-40846-5_33(2069-2079)Online publication date: 27-Apr-2024
https://doi.org/10.1007/978-3-031-40846-5_33
Wagner R(2024)Structural Semiotics as an Ontology of MathematicsHandbook of the History and Philosophy of Mathematical Practice10.1007/978-3-031-40846-5_131(3003-3032)Online publication date: 27-Apr-2024
https://doi.org/10.1007/978-3-031-40846-5_131
Jacobsen FVilladsen J(2023)On Exams with the Isabelle Proof AssistantElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.375.6375(63-76)Online publication date: 10-Mar-2023
https://doi.org/10.4204/EPTCS.375.6
Guo DYu W(2023)A Comprehensive Formalization of Propositional Logic in Coq: Deduction Systems, Meta-Theorems, and Automation TacticsMathematics10.3390/math1111250411:11(2504)Online publication date: 29-May-2023
https://doi.org/10.3390/math11112504
Yan SYu W(2023)Formal Verification of a Topological Spatial Relations Model for Geographic Information Systems in CoqMathematics10.3390/math1105107911:5(1079)Online publication date: 21-Feb-2023
https://doi.org/10.3390/math11051079
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Digital Edition

View this article in digital edition.

Digital Edition

Magazine Site

View this article on the magazine site (external)

Magazine Site

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

A Formally Verified NAT

A Formally Verified Sorting Certifier

Code optimizations using formally verified properties