Over 4000 free audio and video lectures, seminars and teaching resources from Oxford University.
Skip to Content Skip to Navigation

Automating Sized-Type Inference for Complexity Analysis

Loading Video...
Duration: 0:18:50 | Added: 23 Jan 2018
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.

Copy and paste this HTML snippet to embed the audio or video on your site: