PoP Seminar Talk

From Equivalences to Metrics, Effectfully

Ugo Dal Lago, Professor of Computer Science at the University of Bologna
Wednesday, 22 February, 2023; 3:00pm
GHC 8102
Host: Jan Hoffmann

Abstract

Program equivalence is one of the fundamental concepts in the theory of programming languages. In defining the underlying relation, one always strives for compositionality, so that the principle of substitution of equals by equals holds and equational reasoning remains sound. Would it be possible to make equational reasoning compatible with natural generalizations of the notion of equivalence, and with notions of program distance in particular? In this talk, we describe a series of situations in which quantitative reasoning is desirable, together with some proposals for notions of program distance in the style of logical relations and applicative bisimilarity. In doing so, we will focus on higher-order calculi exhibiting some form of computational effect, such as probabilistic choice and cost. In this context, the need for quantitative reasoning is even more urgent, but considerable technical difficulties tend to emerge.

Bio

Ugo Dal Lago is professor of computer science at the University of Bologna, as well as being affiliated with INRIA Sophia Antipolis. His research activity concerns the theory of programming languages and the interactions between logic and computer science. More specifically, he is interested in the quantitative aspects of program semantics, verification, and transformation, with applications to complexity analysis, cryptography, and approximate program transformations.