{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/119582"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/119582","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"Correct-by-construction finite field arithmetic in Coq","abstract":"Elliptic-curve cryptography code, although based on elegant and concise mathematical procedures, often becomes long and complex due to speed optimizations. This statement is especially true for the specialized finite-field libraries used for ECC code, resulting in frequent implementation bugs. I describe the methodologies used to create a Coq framework that generates implementations of finite-field arithmetic routines along with proofs of their correctness, given nothing but the modulus.","abstract_html":"Elliptic-curve cryptography code, although based on elegant and concise mathematical procedures, often becomes long and complex due to speed optimizations. This statement is especially true for the specialized finite-field libraries used for ECC code, resulting in frequent implementation bugs. I describe the methodologies used to create a Coq framework that generates implementations of finite-field arithmetic routines along with proofs of their correctness, given nothing but the modulus.","abstract_has_math":false,"creators":["Philipoom, Jade (Jade D.)"],"institution":"Massachusetts Institute of Technology","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science.","school":null,"contributors":[],"advisors":["Adam Chlipala."],"committee_chairs":[],"committee_members":[],"year":2018,"date_issued":"2018","date_published":"2018","updated_at":"2026-07-22T22:21:06Z","subjects":["Electrical Engineering and Computer Science."],"languages":["eng"],"rights":["MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission."],"rights_urls":["http://dspace.mit.edu/handle/1721.1/7582"],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/1721.1/119582","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Adam Chlipala."]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."]},{"key":"dc:contributor.other","label":"Dc Contributor Other","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."]},{"key":"dc:creator","label":"Author","values":["Philipoom, Jade (Jade D.)"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2018-12-11T20:41:00Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2018-12-11T20:41:00Z"]},{"key":"dc:date.issued","label":"Date","values":["2018"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Electrical Engineering and Computer Science."]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission."]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://dspace.mit.edu/handle/1721.1/7582"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/1721.1/119582"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2018.","This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.","Cataloged from student-submitted PDF version of thesis.","Includes bibliographical references (pages 73-74)."]},{"key":"dc:description.abstract","label":"Abstract","values":["Elliptic-curve cryptography code, although based on elegant and concise mathematical procedures, often becomes long and complex due to speed optimizations. This statement is especially true for the specialized finite-field libraries used for ECC code, resulting in frequent implementation bugs. I describe the methodologies used to create a Coq framework that generates implementations of finite-field arithmetic routines along with proofs of their correctness, given nothing but the modulus."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["M. Eng."]},{"key":"dc:title","label":"Title","values":["Correct-by-construction finite field arithmetic in Coq"]}]}],"canonical_facts":{"dc:contributor.advisor":["Adam Chlipala."],"dc:contributor.department":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."],"dc:contributor.other":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."],"dc:creator":["Philipoom, Jade (Jade D.)"],"dc:date.accessioned":["2018-12-11T20:41:00Z"],"dc:date.available":["2018-12-11T20:41:00Z"],"dc:date.issued":["2018"],"dc:description":["Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2018.","This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.","Cataloged from student-submitted PDF version of thesis.","Includes bibliographical references (pages 73-74)."],"dc:description.abstract":["Elliptic-curve cryptography code, although based on elegant and concise mathematical procedures, often becomes long and complex due to speed optimizations. This statement is especially true for the specialized finite-field libraries used for ECC code, resulting in frequent implementation bugs. I describe the methodologies used to create a Coq framework that generates implementations of finite-field arithmetic routines along with proofs of their correctness, given nothing but the modulus."],"dc:description.degree":["M. Eng."],"dc:identifier.uri":["http://hdl.handle.net/1721.1/119582"],"dc:language.iso":["eng"],"dc:publisher":["Massachusetts Institute of Technology"],"dc:rights":["MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission."],"dc:rights.uri":["http://dspace.mit.edu/handle/1721.1/7582"],"dc:subject":["Electrical Engineering and Computer Science."],"dc:title":["Correct-by-construction finite field arithmetic in Coq"],"dc:type":["Thesis"]},"updated_at":"2026-07-22T22:21:06Z"}