文章基本信息

标题：Cost Recurrences for DML Programs
本地全文：下载
作者：Bernd Grobauer
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：2001
卷号：8
期号：25
出版社：Aarhus University
摘要：A cost recurrence describes an upper bound for the running time of a program in terms of the size of its input. Finding cost recurrences is a frequent intermediate step in complexity analysis, and this step requires an abstraction from data to data size. In this article, we use information contained in dependent types to achieve such an abstraction: Dependent ML (DML), a conservative extension of ML, provides dependent types that can be used to associate data with size information, thus describing a possible abstraction. We systematically extract cost recurrences from first-order DML programs, guiding the abstraction from data to data size with information contained in DML type derivations.