This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three components: A powerful type system for size analysis and a sound type inference procedure for it, a ticking monadic transformation and a concrete tool for 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 various key ingredients, and in particular an abstract index language and index polymorphism at higher ranks. A prototype implementation is available.
Automating sized-Type inference and complexity analysis / Avanzini, Martin; Ugo Dal, Lago. - In: ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE. - ISSN 2075-2180. - ELETTRONICO. - 248:(2017), pp. 7-16. (Intervento presentato al convegno 8th Workshop on Developments in Implicit Computational ComplExity and 5th Workshop on FOundational and Practical Aspects of Resource Analysis, DICE-FOPARA 2017 tenutosi a Uppsala, Sweden nel 2017) [10.4204/EPTCS.248.5].
Automating sized-Type inference and complexity analysis
Avanzini, Martin;Lago, Ugo Dal
2017
Abstract
This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three components: A powerful type system for size analysis and a sound type inference procedure for it, a ticking monadic transformation and a concrete tool for 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 various key ingredients, and in particular an abstract index language and index polymorphism at higher ranks. A prototype implementation is available.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
