Proving formally the implementation of an efficient gcd algorithm for polynomials

Assia Mahboubi

doi:10.1007/11814771_37

Proving formally the implementation of an efficient gcd algorithm for polynomials

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

Abstract

We describe here a formal proof in the Coq system of the structure theorem for subresultants, which allows to prove formally the correctness of our implementation of the subresultants algorithm. Up to our knowledge it is the first mechanized proof of this result. © Springer-Verlag Berlin Heidelberg 2006.

Original language	English
Title of host publication	Automated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings
Publisher	Springer Verlag
Pages	438-452
ISBN (Print)	3540371877, 9783540371878
DOIs	https://doi.org/10.1007/11814771_37
Publication status	Published - 2006
Externally published	Yes
Event	Third International Joint Conference on Automated Reasoning, IJCAR 2006 - , United States Duration: 17 Aug 2006 → 20 Aug 2006

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	Third International Joint Conference on Automated Reasoning, IJCAR 2006
Country/Territory	United States
Period	17/08/06 → 20/08/06

Access to Document

10.1007/11814771_37

Persistent URL (handle)

Persistent link

Cite this

Mahboubi, A. (2006). Proving formally the implementation of an efficient gcd algorithm for polynomials. In Automated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings (pp. 438-452). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Springer Verlag. https://doi.org/10.1007/11814771_37

@inproceedings{5742cf9886304d43a2a3361bd4970d39,

title = "Proving formally the implementation of an efficient gcd algorithm for polynomials",

abstract = "We describe here a formal proof in the Coq system of the structure theorem for subresultants, which allows to prove formally the correctness of our implementation of the subresultants algorithm. Up to our knowledge it is the first mechanized proof of this result. {\textcopyright} Springer-Verlag Berlin Heidelberg 2006.",

author = "Assia Mahboubi",

year = "2006",

doi = "10.1007/11814771_37",

language = "English",

isbn = "3540371877",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "438--452",

booktitle = "Automated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings",

note = "Third International Joint Conference on Automated Reasoning, IJCAR 2006 ; Conference date: 17-08-2006 Through 20-08-2006",

}

Mahboubi, A 2006, Proving formally the implementation of an efficient gcd algorithm for polynomials. in Automated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Verlag, pp. 438-452, Third International Joint Conference on Automated Reasoning, IJCAR 2006, United States, 17/08/06. https://doi.org/10.1007/11814771_37

Proving formally the implementation of an efficient gcd algorithm for polynomials. / Mahboubi, Assia.
Automated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings. Springer Verlag, 2006. p. 438-452 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Proving formally the implementation of an efficient gcd algorithm for polynomials

AU - Mahboubi, Assia

PY - 2006

Y1 - 2006

N2 - We describe here a formal proof in the Coq system of the structure theorem for subresultants, which allows to prove formally the correctness of our implementation of the subresultants algorithm. Up to our knowledge it is the first mechanized proof of this result. © Springer-Verlag Berlin Heidelberg 2006.

AB - We describe here a formal proof in the Coq system of the structure theorem for subresultants, which allows to prove formally the correctness of our implementation of the subresultants algorithm. Up to our knowledge it is the first mechanized proof of this result. © Springer-Verlag Berlin Heidelberg 2006.

UR - http://www.scopus.com/inward/record.url?scp=33749561415&partnerID=8YFLogxK

U2 - 10.1007/11814771_37

DO - 10.1007/11814771_37

M3 - Conference contribution

SN - 3540371877

SN - 9783540371878

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 438

EP - 452

BT - Automated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings

PB - Springer Verlag

T2 - Third International Joint Conference on Automated Reasoning, IJCAR 2006

Y2 - 17 August 2006 through 20 August 2006

ER -

Mahboubi A. Proving formally the implementation of an efficient gcd algorithm for polynomials. In Automated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings. Springer Verlag. 2006. p. 438-452. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/11814771_37

Proving formally the implementation of an efficient gcd algorithm for polynomials

Abstract

Publication series

Conference

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this