DiscoverInternational Conference on Functional Programming 2017Automating Sized-Type Inference for Complexity Analysis
Automating Sized-Type Inference for Complexity Analysis

Automating Sized-Type Inference for Complexity Analysis

Update: 2018-01-23
Share

Description

Martin Avanzini (University of Innsbruck, Austria) gives the second talk in the fifth panel, Inference and Analysis on the 3rd day of the ICFP conference. 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 various key ingredients, and in particular an abstract index language and index polymorphism at higher ranks. A prototype implementation is available. Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/
Comments 
loading
00:00
00:00
1.0x

0.5x

0.8x

1.0x

1.25x

1.5x

2.0x

3.0x

Sleep Timer

Off

End of Episode

5 Minutes

10 Minutes

15 Minutes

30 Minutes

45 Minutes

60 Minutes

120 Minutes

Automating Sized-Type Inference for Complexity Analysis

Automating Sized-Type Inference for Complexity Analysis

Martin Avanzini