Introduction to Mathematical Components

DOI Web Site Open Access
  • AFFELDT Reynald
    Information Technology Research Institute, National Institute of Advanced Industrial Science and Technology

Bibliographic Information

Other Title
  • Mathematical Components入門
  • Mathematical Components ニュウモン

Search this article

Abstract

Since 1969 and the Curry-Howard isomorphism, we know that there is a strong relation between computer programs and mathematical proofs: concretely, if we look at the type of a program as a mathematical statement, then the program itself can be regarded as a proof. As a consequence, proof-checking can be performed by type-checking. Based on this theoretical idea, verification tools have been developed that are now mature enough to tackle non-trivial formal verification tasks.<BR>The formal verification of the odd order theorem, conducted from 2005 to 2012 by Microsoft Research-INRIA, is an example of realistic formal verification. It became a milestone because this theorem is an important result of group theory whose proof is particularly large. But in fact, the formal libraries known as the Mathematical Components that form the basis of this formalization are an equally important output of this experiment.<BR>Indeed, using the Mathematical Components, it becomes possible to carry out rigorous verifications of computer programs that rely on non-trivial mathematics. Such programs are actually important parts of our digitial society. One can think for example of RSA encryption or elliptic-curve cryptography, that are based on number theory, group theory, linear algebra, etc.<BR>Still, the Mathematical Components form a huge library whose usage requires specific expertise. In this introductory paper, we explain the basics of the Mathematical Components, using as a running example the Lagrange theorem.

Journal

  • Computer Software

    Computer Software 34 (2), 2_64-2_74, 2017

    Japan Society for Software Science and Technology

Related Projects

See more

Details 詳細情報について

Report a problem

Back to top