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
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:	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:	05 Nov 2024 11:05 UTC
Resource URI:	https://kar.kent.ac.uk/id/eprint/66330 (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):

Altmetric

Download Statistics

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