Formal proof of polynomial-time complexity with quasi-interpretations
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Standard
Formal proof of polynomial-time complexity with quasi-interpretations. / Férée, Hugo; Hym, Samuel; Mayero, Micaela; Moyen, Jean Yves; Nowak, David.
CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018. Association for Computing Machinery, 2018. p. 146-157.Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - Formal proof of polynomial-time complexity with quasi-interpretations
AU - Férée, Hugo
AU - Hym, Samuel
AU - Mayero, Micaela
AU - Moyen, Jean Yves
AU - Nowak, David
PY - 2018
Y1 - 2018
N2 - We present a Coq library that allows for readily proving that a function is computable in polynomial time. It is based on quasi-interpretations that, in combination with termination ordering, provide a characterisation of the class FP of functions computable in polynomial time. At the heart of this formalisation is a proof of soundness and extensional completeness. Compared to the original paper proof, we had to fill a lot of not so trivial details that were left to the reader and fix a few glitches. To demonstrate the usability of our library, we apply it to the modular exponentiation.
AB - We present a Coq library that allows for readily proving that a function is computable in polynomial time. It is based on quasi-interpretations that, in combination with termination ordering, provide a characterisation of the class FP of functions computable in polynomial time. At the heart of this formalisation is a proof of soundness and extensional completeness. Compared to the original paper proof, we had to fill a lot of not so trivial details that were left to the reader and fix a few glitches. To demonstrate the usability of our library, we apply it to the modular exponentiation.
KW - Coq formal proof
KW - Implicit complexity
KW - Polynomial time
UR - http://www.scopus.com/inward/record.url?scp=85044279141&partnerID=8YFLogxK
U2 - 10.1145/3167097
DO - 10.1145/3167097
M3 - Article in proceedings
AN - SCOPUS:85044279141
SP - 146
EP - 157
BT - CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018
PB - Association for Computing Machinery
T2 - 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018
Y2 - 8 January 2018 through 9 January 2018
ER -
ID: 203774824