Certifying and Reasoning on Cost Annotations of Functional Programs

DOI10.1007/978-3-642-32495-6_5MaRDI QIDQ3167527zbMATH OpenOpenAlexFDO

Authors Roberto M. Amadio, Yann Régis-Gianas

Publication date 2 November 2012

Published in Foundational and Practical Aspects of Resource Analysis (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1110.2350

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Abstract: We present a so-called labelling method to insert cost annotations in a higher-order functional program, to certify their correctness with respect to a standard compilation chain to assembly code including safe memory management, and to reason on them in a higher-order Hoare logic.

Recommendations

• scientific article; zbMATH DE number 512849
• Implementation of Functional Languages
• Automating relatively complete verification of higher-order functional programs
• Cost-sensitive diagnosis of declarative programs
• Producing certified functional code from inductive specifications
• Denotational semantics as a foundation for cost recurrence extraction for functional languages
• Problems of verification of functional programs

Cited in

(3)

• The verified CakeML compiler backend
• Indexed labels for loop iteration dependent costs
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits

This page was built for publication: Certifying and Reasoning on Cost Annotations of Functional Programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3167527)