Automating sized-Type inference for complexity analysis

被引：18

作者：

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 条

[1]

Abel A., Pientka B., Well-founded recursion with copatterns and sized types, JFP, 26, (2016)

[2]

Albert E., Arenas P., Genaim S., Puebla G., Automatic inference of upper bounds for recurrence relations in cost analysis, SAS, pp. 221-237, (2008)

[3]

Albert E., Genaim S., Masud A.N., On the inference of resource usage upper and lower bounds, TOCL, 14, 3, (2013)

[4]

Aspinall D., Beringer L., Hofmann M., Loidl H.-W., Momigliano A., A program logic for resources, TCS, 389, 3, pp. 411-445, (2007)

[5]

Avanzini M., Dal Lago U., Automating Sized Type Inference for Complexity Analysis, pp. 1-38, (2017)

[6]

Avanzini M., Dal Lago U., Moser G., Analysing the complexity of functional programs: Higher-order meets first-order, ICFP, pp. 152-164, (2015)

[7]

Avanzini M., Moser G., Closing the gap between runtime complexity and polytime computability, RTA (LIPIcs), 6, pp. 33-48, (2010)

[8]

Avanzini M., Moser G., Schaper M., TcT: Tyrolean complexity tool, TACAS (LNCS), pp. 407-423, (2016)

[9]

Barthe G., Gregoire B., Riba C., Type-based termination with sized products, CSL (LNCS), 5213, pp. 493-507, (2008)

[10]

Blanqui F., Decidability of type-checking in the calculus of algebraic constructions with size annotations, CSL (LNCS), 3634, pp. 135-150, (2005)

← 1 2 3 4 →