Automating sized-Type inference for complexity analysis

被引:18
作者
Avanzini M. [1 ]
Dal Lago U. [2 ,3 ]
机构
[1] Avanzini, Martin
[2] 2,Dal Lago, Ugo
关键词
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)