Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/ ZENODOarrow_drop_down
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Article . 2023
License: CC BY ND
Data sources: Datacite
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Conference object . 2023
License: http://creativecommons.org/licenses/by-nd/4.0/legalcode
Data sources: ZENODO
Hal; Mémoires en Sciences de l'Information et de la Communication
Preprint . 2023
License: CC BY
Full-Text: https://hal.science/hal-04083105/document
Data sources: Mémoires en Sciences de l'Information et de la Communication; Hal
 View all 4 versions
Claim

This Research product is the result of merged Research products in OpenAIRE.

You have already added 0 works in your ORCID record related to the merged Research product.

Certifying Complexity Analysis

descriptionPublicationkeyboard_double_arrow_right Preprint , Article , Conference object 21 Jan 2023Publisher:Zenodo
Authors: Aubert, Clément; Rubiano, Thomas; Rusch, Neea; Seiller, Thomas;

doi: 10.5281/zenodo.7938772 , 10.5281/zenodo.7938773

Certifying Complexity Analysis

Abstract

This work drafts a strategy that leverages the field of Implicit Computational Complexity to certify resource usage in imperative programs. This original approach sidesteps some of the most common–and difficult–obstacles “traditional” complexity theory face when implemented in Coq.

Communication at the Ninth International Workshop on Coq for Programming Languages (CoqPL 2023).

Keywords

Program verification in Coq, [INFO.INFO-CC]Computer Science [cs]/Computational Complexity [cs.CC], Complexity theory and logic, Program verification, Theory of computation

Powered by OpenAIRE graph
Found an issue? Give us feedback