Online learning algorithms often rely on randomness, their loss functions are often defined as expectations, precise bounds are often non-polynomial (e.g., logarithmic) and proofs of optimality often rely on potential (ranking function) based arguments. In this talk, I will present pλ-amor, a type-theoretic graded modal framework for analysing expected cost properties of higher-order probabilistic programs with recursion. pλ-amor is an effect-based framework which uses graded modal types to represent potentials, cost and probability at the type level. It extends prior work (λ-amor) on cost analysis for deterministic programs. We prove pλ-amor sound relative to a Kripke step-indexed model which relates potentials with probabilistic coupling. pλ-amor is also quite expressive, we have used pλ-amor to prove cost bounds of several examples from the machine learning literature, and also describe an embedding of a coeffect-based type theory in pλ-amor.

Vineet Rajani is a lecturer in the School of Computing at the University of Kent. At Kent, he is affiliated with both the Programming languages and the Cyber security group. Vineet joined Kent, after finishing his postdoc and PhD from Max Planck Institute - for Security and Privacy, and Software Systems, respectively. Vineet's interest lies in the development of formal and provably correct methods to reason about properties of computation, especially those pertaining to security and quantitative resource bounds. His work on secure information flow has won distinguished paper awards at premier venues of security foundations (CSF'18) and programming languages (POPL'19) research.