-
- 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
- Tweet
Details 詳細情報について
-
- CRID
- 1390001204737348480
-
- NII Article ID
- 40021209938
- 130006855229
-
- NII Book ID
- AN10075819
-
- NDL BIB ID
- 028211535
-
- ISSN
- 02896540
-
- Text Lang
- ja
-
- Data Source
-
- JaLC
- NDL
- CiNii Articles
- KAKEN
-
- Abstract License Flag
- Disallowed