Document Type

Other

Publication Date

2013

Abstract

The files in this directory comprise a formal development in Coq of a target language, complexity language, translation, and soundness theorem, all of which combine to provide a mechanism for certified cost bounds on higher-order programs. This section is intended to contain the most current version of the development, which may or may not correspond directly to the developments associated with particular papers from this project.

Comments

Associated papers:

Danner, N., Paykin, J. and Royer, J.S. A static cost analysis of a higher-order language. To appear in Proceedings of the Seventh Workshop on Programming Languages Meets Program Verification, 2013.

Share

COinS