skip to main content
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
  • (2016)A Mechanized Textbook Proof of a Type Unification AlgorithmFormal Methods: Foundations and Applications10.1007/978-3-319-29473-5_8(127-141)Online publication date: 24-Jan-2016
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

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
  • 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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013
Published in SIGPLAN Volume 48, Issue 1

Check for updates

Author Tags

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

Qualifiers

  • Keynote

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
  • (2016)A Mechanized Textbook Proof of a Type Unification AlgorithmFormal Methods: Foundations and Applications10.1007/978-3-319-29473-5_8(127-141)Online publication date: 24-Jan-2016
  • (2013)Mechanized metatheory for a $$\lambda $$ λ -calculus with trust typesJournal of the Brazilian Computer Society10.1007/s13173-013-0119-519:4(433-443)Online publication date: 4-Aug-2013
  • (2013)Exploring Automated Reasoning in First-Order Logic: Tools, Techniques and Application AreasKnowledge Engineering and the Semantic Web10.1007/978-3-642-41360-5_9(102-116)Online publication date: 2013
  • (2013)Communicating formal proofsProceedings of the 4th international conference on Interactive Theorem Proving10.1007/978-3-642-39634-2_32(451-456)Online publication date: 22-Jul-2013
  • (2013)Mathematical practice, crowdsourcing, and social machinesProceedings of the 2013 international conference on Intelligent Computer Mathematics10.1007/978-3-642-39320-4_7(98-119)Online publication date: 8-Jul-2013
  • (2013)Formal mathematics on displayProceedings of the 2013 international conference on Intelligent Computer Mathematics10.1007/978-3-642-39320-4_10(152-167)Online publication date: 8-Jul-2013
  • (2013)Formal Verification of a C Value Analysis Based on Abstract InterpretationStatic Analysis10.1007/978-3-642-38856-9_18(324-344)Online publication date: 2013
  • (2013)Certified Impossibility Results for Byzantine-Tolerant Mobile RobotsStabilization, Safety, and Security of Distributed Systems10.1007/978-3-319-03089-0_13(178-190)Online publication date: 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