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

Férée, H, Hym, S, Mayero, M, Moyen, JY & Nowak, D 2018, Formal proof of polynomial-time complexity with quasi-interpretations. in CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018. Association for Computing Machinery, pp. 146-157, 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, United States, 08/01/2018. https://doi.org/10.1145/3167097

APA

Férée, H., Hym, S., Mayero, M., Moyen, J. Y., & Nowak, D. (2018). Formal proof of polynomial-time complexity with quasi-interpretations. In CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018 (pp. 146-157). Association for Computing Machinery. https://doi.org/10.1145/3167097

Vancouver

Férée H, Hym S, Mayero M, Moyen JY, Nowak D. Formal proof of polynomial-time complexity with quasi-interpretations. In 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 https://doi.org/10.1145/3167097

Author

Férée, Hugo ; Hym, Samuel ; Mayero, Micaela ; Moyen, Jean Yves ; Nowak, David. / Formal proof of polynomial-time complexity with quasi-interpretations. 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. pp. 146-157

Bibtex

@inproceedings{9f193ec774a04a6fa40d9593adab8059,
title = "Formal proof of polynomial-time complexity with quasi-interpretations",
abstract = "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.",
keywords = "Coq formal proof, Implicit complexity, Polynomial time",
author = "Hugo F{\'e}r{\'e}e and Samuel Hym and Micaela Mayero and Moyen, {Jean Yves} and David Nowak",
year = "2018",
doi = "10.1145/3167097",
language = "English",
pages = "146--157",
booktitle = "CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018",
publisher = "Association for Computing Machinery",
note = "7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018 ; Conference date: 08-01-2018 Through 09-01-2018",

}

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