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)

PDF - Author's Accepted Manuscript
Restricted to Repository staff only
Contact us about this Publication Download (263kB)
[img]
Official URL
http://dx.doi.org/10.1145/3167097

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.

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: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Hugo Feree
Date Deposited: 09 Mar 2018 13:32 UTC
Last Modified: 24 Sep 2019 09:25 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/66330 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year