CS Colloquium - Ugo Dal Lago, University of Bologna, Italy

Event time: 
Tuesday, February 6, 2024 - 4:00pm
AKW 200 See map
51 Prospect Street
New Haven, CT 06511
Event description: 

CS Colloquium
Ugo Dal Lago
University of Bologna, Italy

Host: Zhong Shao

Title: From Equivalences to Metrics, Effectfully


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.