LFCS Seminar: Thursday 5th June: Rasmus Møgelberg

Title: Induction and Recursion Principles in a Higher-Order Quantitative Logic

Abstract: Quantitative logic reasons about the degree to which

formulas are satisfied. This paper studies the fundamental

reasoning principles of higher-order quantitative logic and their

application to reasoning about probabilistic programs and processes.

We construct an affine calculus for 1-bounded complete metric

spaces and the monad for probability measures equipped with

the Kantorovic distance. The calculus includes a form of guarded

recursion interpreted via Banach’s fixed point theorem, useful,

e.g., for recursive programming with processes. We then define an

affine higher-order quantitative logic for reasoning about terms

of our calculus. The logic includes novel principles for guarded

recursion, and induction over probability measures and natural

numbers.

Examples of reasoning in the logic include proofs of upper

bounds on distances of processes. We also show how our logic can

express coupling proofs —a powerful technique for comparing

probabilistic processes.

The talk is based on joint work with Giorgio Bacci.