Skip to Main content Skip to Navigation
Conference papers

Type-Based Complexity Analysis of Probabilistic Functional Programs

Martin Avanzini 1 Ugo Dal Lago 1 Alexis Ghyselen 2
1 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : We show that complexity analysis of probabilistic higher-order functional programs can be carried out composi-tionally by way of a type system. The introduced type system is a significant extension of refinement types. On the one hand, the presence of probabilistic effects requires adopting a form of dynamic distribution type, subject to a coupling-based subtyping discipline. On the other hand, recursive definitions are proved terminating by way of Lyapunov ranking functions. We prove not only that the obtained type system, called RPCF, provides a sound methodology for average case complexity analysis, but also that it is extensionally complete, in the sense that any average case polytime Turing machines can be encoded as a term typable in RPCF.
Document type :
Conference papers
Complete list of metadata

Cited literature [41 references]  Display  Hide  Download
Contributor : Martin Avanzini <>
Submitted on : Wednesday, November 27, 2019 - 3:57:53 PM
Last modification on : Friday, October 30, 2020 - 12:04:04 PM
Long-term archiving on: : Friday, February 28, 2020 - 1:15:43 PM


Files produced by the author(s)




Martin Avanzini, Ugo Dal Lago, Alexis Ghyselen. Type-Based Complexity Analysis of Probabilistic Functional Programs. LICS 2019 - 34th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2019, Vancouver, Canada. pp.1-13, ⟨10.1109/LICS.2019.8785725⟩. ⟨hal-02381829⟩



Record views


Files downloads