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, and to reason on them in a higher-order Hoare logic.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Amadio, R.M., Ayache, N., Régis-Gianas, Y., Saillard, R.: Certifying cost annotations in compilers. Université Paris Diderot, Research Report (2010), http://hal.archives-ouvertes.fr/hal-00524715/fr/
Amadio, R.M., Régis-Gianas, Y.: Certifying and reasoning on cost annotations of functional programs Université Paris Diderot, Research Report (2011), http://hal.inria.fr/inria-00629473/en/
AbsInt Angewandte Informatik, http://www.absint.com/
Bonenfant, A., Ferdinand, C., Hammond, K., Heckmann, R.: Worst-Case Execution Times for a Purely Functional Language. In: Horváth, Z., Zsók, V., Butterfield, A. (eds.) IFL 2006. LNCS, vol. 4449, pp. 235–252. Springer, Heidelberg (2007)
Chlipala, A.: A verified compiler for an impure functional language. In: Proc. ACM-POPL, pp. 93–106 (2010)
The Coq Development Team. The Coq Proof Assistant. INRIA-Rocquencourt (December 2001), http://coq.inria.fr
Gurr, D.: Semantic frameworks for complexity. PhD thesis, University of Edinburgh (1991)
Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)
Morrisett, J., Walker, D., Crary, K., Glew, N.: From system F to typed assembly language. ACM Trans. Program. Lang. Syst. 21(3), 527–568 (1999)
Perlis, A.: Epigrams on programming. SIGPLAN Notices 17(9), 7–13 (1982)
Plotkin, G.: Call-by-name, Call-by-value and the lambda-Calculus. Theor. Comput. Sci. 1(2), 125–159 (1975)
Régis-Gianas, Y., Pottier, F.: A Hoare Logic for Call-by-Value Functional Programs. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol. 5133, pp. 305–335. Springer, Heidelberg (2008)
Sands, D.: Complexity Analysis for a Lazy Higher-Order Language. In: Jones, N.D. (ed.) ESOP 1990. LNCS, vol. 432, pp. 361–376. Springer, Heidelberg (1990)
Régis-Gianas, Y.: An annotating compiler for MiniML, http://www.pps.jussieu.fr/~yrg/fun-cca
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Amadio, R.M., Régis-Gianas, Y. (2012). Certifying and Reasoning on Cost Annotations of Functional Programs. In: Peña, R., van Eekelen, M., Shkaravska, O. (eds) Foundational and Practical Aspects of Resource Analysis. FOPARA 2011. Lecture Notes in Computer Science, vol 7177. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32495-6_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-32495-6_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32494-9
Online ISBN: 978-3-642-32495-6
eBook Packages: Computer ScienceComputer Science (R0)