Certifying and reasoning about cost annotations of functional programs
classification
💻 cs.PL
keywords
annotationscostfunctionalhigher-orderassemblycertifycertifyingchain
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.