CS Colloquium
Ugo Dal Lago
University of Bologna, Italy
Host: Zhong Shao
Title: From Equivalences to Metrics, Effectfully
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.