Skip to main content

Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations

Férée, Hugo, Hym, Samuel, Mayero, Micaela, Moyen, Jean-Yves, 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. . ACM 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)

PDF - Author's Accepted Manuscript
Restricted to Repository staff only
Contact us about this Publication Download (263kB)
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: Conference or workshop item (Proceeding)
DOI/Identification number: 10.1145/3167097
Uncontrolled keywords: Coq formal proof, implicit complexity, polynomial time
Divisions: Faculties > Sciences > School of Computing
Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Hugo Feree
Date Deposited: 09 Mar 2018 13:32 UTC
Last Modified: 29 May 2019 20:21 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year