Automating sized-Type inference for complexity analysis

被引：19

作者：

Avanzini M. ^{[1
]}

Dal Lago U. ^{[2
,3
]}

机构：

[1] Avanzini, Martin

[2] 2,Dal Lago, Ugo

来源：

| 2017年 / Association for Computing Machinery卷 / 01期

关键词：

Automation; Runtime complexity analysis; Sized types;

D O I：

10.1145/3110287

中图分类号：

学科分类号：

摘要：

This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three ingredients: a powerful type system for size analysis and a sound type inference procedure for it, a ticking monadic transformation, and constraint solving. Noticeably, the presented methodology can be fully automated, and is able to analyse a series of examples which cannot be handled by most competitor methodologies. This is possible due to the choice of adopting an abstract index language and index polymorphism at higher ranks. A prototype implementation is available. © 2017 Copyright held by the owner/author(s).

引用

共 38 条

[21]

Hoffmann J., Aehlig K., Hofmann M., Multivariate amortized resource analysis, POPL, pp. 357-370, (2011)

[22]

Hoffmann J., Aehlig K., Hofmann M., Resource aware ML, CAV (LNCS), 7358, pp. 781-786, (2012)

[23]

Hoffmann J., Das A., Weng S.-C., Towards automatic resource bound analysis for OCaml, POPL, pp. 359-373, (2017)

[24]

Hoffmann J., Shao Z., Automatic static cost analysis for parallel programs, ESOP (LNCS), 9032, pp. 132-157, (2015)

[25]

Hoffmann J., Shao Z., Type-based amortized resource analysis with integers and arrays, JFP, 25, (2015)

[26]

Hughes J., Pareto L., Sabry A., Proving the correctness of reactive systems using sized types, POPL (POPL’96), pp. 410-423, (1996)

[27]

Jost S., Hammond K., Loidl H.-W., Hofmann M., Static determination of quantitative resource usage for higher-order programs, POPL, pp. 223-236, (2010)

[28]

Mendonca De Moura L., Bjurner N., Z3: An efficient SMT solver, TACAS (LNCS), 4963, pp. 337-340, (2008)

[29]

Mycroft A., Polymorphic Type Schemes and Recursive Definitions, pp. 217-228, (1984)

[30]

Okasaki C., Purely Functional Data Structures, (1999)

← 1 2 3 4 →