Proof Techniques for Program Equivalence in Probabilistic Higher-Order Languages (Invited Talk)

Abstract

While the theory of functional higher-order languages, starting from lambda-calculi, is a well-established research field, it is only in recent years that the operational semantics of higher-order languages with probabilistic operators has started to be extensively studied. A fundamental notion in the semantics of programming languages is that of program equivalence. In higher-order languages, program equivalence is generally formalized as a contextual equivalence [Morris, 1968], which can be hard to prove directly. This has motivated the study of proof techniques for contextual equivalence, from inductive ones, such as logical relations [Andrew Pitts, 2005], to coinductive ones, mainly in the form of bisimulations [Abramsky, 1990]. In this talk I will discuss proof techniques for program equivalence in languages combining higher-order and probabilistic features. Several operational methods, traditionally developed in a deterministic setting, have been adapted to probabilistic higher-order languages [Ales Bizjak and Lars Birkedal, 2015; Dal Lago et al., 2014; Raphaëlle Crubillé and Ugo Dal Lago, 2014]. I will discuss these proof methods and focus on bisimulation-based techniques, showing how probabilities, combined with different language features, force a number of modifications to the definition of bisimulation [Crubillé et al., 2015; Sangiorgi and Vignudelli, 2016].