skip to main content
10.1145/2429069.2429071acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
keynote

Engineering mathematics: the odd order theorem proof

Published: 23 January 2013 Publication History

Abstract

Even with the assistance of computer tools, the formalized de-scription and verification of research-level mathematics remains a daunting task, not least because of the talent with which mathema-ticians combine diverse theories to achieve their ends. By combin-ing tools and techniques from type theory, language design, and software engineering we have managed to capture enough of these practices to formalize the proof of the Odd Order theorem, a landmark result in Group Theory.

Supplementary Material

JPG File (r1d1_talk2.jpg)
MP4 File (r1d1_talk2.mp4)

Cited By

View all
  • (2019)Formal Methods for Mobile RobotsDistributed Computing by Mobile Entities10.1007/978-3-030-11072-7_12(278-313)Online publication date: 13-Jan-2019
  • (2016)Towards Formal Proof MetricsProceedings of the 19th International Conference on Fundamental Approaches to Software Engineering - Volume 963310.1007/978-3-662-49665-7_19(325-341)Online publication date: 2-Apr-2016
  • (2015)Formalizing PhysicsProceedings of the International Conference on Intelligent Computer Mathematics - Volume 915010.1007/978-3-319-20615-8_19(288-295)Online publication date: 13-Jul-2015
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2013
586 pages
ISBN:9781450318327
DOI:10.1145/2429069
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 48, Issue 1
    POPL '13
    January 2013
    561 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/2480359
    Issue’s Table of Contents

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. coq
  2. group theory
  3. mathematical components
  4. proof engineering
  5. ssreflect.
  6. theorem proving

Qualifiers

  • Keynote

Conference

POPL '13
Sponsor:

Acceptance Rates

Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)7
  • Downloads (Last 6 weeks)0
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2019)Formal Methods for Mobile RobotsDistributed Computing by Mobile Entities10.1007/978-3-030-11072-7_12(278-313)Online publication date: 13-Jan-2019
  • (2016)Towards Formal Proof MetricsProceedings of the 19th International Conference on Fundamental Approaches to Software Engineering - Volume 963310.1007/978-3-662-49665-7_19(325-341)Online publication date: 2-Apr-2016
  • (2015)Formalizing PhysicsProceedings of the International Conference on Intelligent Computer Mathematics - Volume 915010.1007/978-3-319-20615-8_19(288-295)Online publication date: 13-Jul-2015
  • (2013)Certified Impossibility Results for Byzantine-Tolerant Mobile Robots15th International Symposium on Stabilization, Safety, and Security of Distributed Systems - Volume 825510.5555/2718693.2718706(178-190)Online publication date: 13-Nov-2013
  • (2013)Handlers in actionACM SIGPLAN Notices10.1145/2544174.250059048:9(145-158)Online publication date: 25-Sep-2013
  • (2013)C-SHOReACM SIGPLAN Notices10.1145/2544174.250058948:9(13-24)Online publication date: 25-Sep-2013
  • (2013)Higher-order functional reactive programming without spacetime leaksACM SIGPLAN Notices10.1145/2544174.250058848:9(221-232)Online publication date: 25-Sep-2013
  • (2013)Modular monadic meta-theoryACM SIGPLAN Notices10.1145/2544174.250058748:9(319-330)Online publication date: 25-Sep-2013
  • (2013)An operational foundation for the tactic language of CoqProceedings of the 15th Symposium on Principles and Practice of Declarative Programming10.1145/2505879.2505890(25-36)Online publication date: 16-Sep-2013
  • (2013)Modular monadic meta-theoryProceedings of the 18th ACM SIGPLAN international conference on Functional programming10.1145/2500365.2500587(319-330)Online publication date: 25-Sep-2013
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media