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

Datalogisk Institut

1 Citationer (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.

Originalsprog	Engelsk
Titel	CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018
Forlag	Association for Computing Machinery
Publikationsdato	2018
Sider	146-157
ISBN (Elektronisk)	9781450355865
DOI	https://doi.org/10.1145/3167097
Status	Udgivet - 2018
Begivenhed	7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018 - Los Angeles, USA Varighed: 8 jan. 2018 → 9 jan. 2018

Konference

Konference	7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018
Land/Område	USA
By	Los Angeles
Periode	08/01/2018 → 09/01/2018
Sponsor	ACM SIGPLAN

Adgang til dokumentet

10.1145/3167097

Andre filer og links

Link to publication in Scopus

Citationsformater

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. s. 146-157.

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

Férée, H, Hym, S, Mayero, M, Moyen, JY & Nowak, D 2018, Formal proof of polynomial-time complexity with quasi-interpretations. i CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018. Association for Computing Machinery, s. 146-157, 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, USA, 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

Konference

Adgang til dokumentet

Andre filer og links

Fingeraftryk

Citationsformater