Formal proof of polynomial-time complexity with quasi-interpretations

Hugo Férée; Samuel Hym; Micaela Mayero; Jean Yves Moyen; David Nowak

doi:10.1145/3167097

Formal proof of polynomial-time complexity with quasi-interpretations

Hugo Férée, Samuel Hym, Micaela Mayero, Jean Yves Moyen, David Nowak

Department of Computer Science

1 Citation (Scopus)

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.

Original language	English
Title of host publication	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
Publication date	2018
Pages	146-157
ISBN (Electronic)	9781450355865
DOIs	https://doi.org/10.1145/3167097
Publication status	Published - 2018
Event	7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018 - Los Angeles, United States Duration: 8 Jan 2018 → 9 Jan 2018

Conference

Conference	7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018
Country/Territory	United States
City	Los Angeles
Period	08/01/2018 → 09/01/2018
Sponsor	ACM SIGPLAN

Keywords

Coq formal proof
Implicit complexity
Polynomial time

Access to Document

10.1145/3167097

Cite this

Formal proof of polynomial-time complexity with quasi-interpretations. / Férée, Hugo; Hym, Samuel; Mayero, Micaela et al.

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

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

@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",

}

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 -

Formal proof of polynomial-time complexity with quasi-interpretations

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this