Skip to main content

Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations

Férée, Hugo and Hym, Samuel and Mayero, Micaela and Moyen, Jean-Yves and Nowak, David (2018) Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. POPL Principles of Programming Languages . ACM, New York, USA. ISBN 978-1-4503-5586-5. (doi:10.1145/3167097) (Access to this publication is currently restricted. You may be able to access a copy if URLs are provided) (KAR id:66330)

PDF Author's Accepted Manuscript
Language: English

Restricted to Repository staff only
Contact us about this Publication
[thumbnail of cpp2018.pdf]
Official URL:


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.

Item Type: Book section
DOI/Identification number: 10.1145/3167097
Uncontrolled keywords: Coq formal proof, implicit complexity, polynomial time
Subjects: Q Science > QA Mathematics (inc Computing science)
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Hugo Feree
Date Deposited: 09 Mar 2018 13:32 UTC
Last Modified: 16 Feb 2021 13:53 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

Férée, Hugo.

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.