2026-07-23T18:08:48Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9174 2024-03-06T10:43:32Z ddc:004 open_access

Proof Techniques for Program Equivalence in Probabilistic Higher-Order Languages (Invited Talk) Vignudelli, Valeria Lambda Calculus Contextual Equivalence Bisimulation Probabilistic Programming Languages 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]. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Valeria Vignudelli 2018 Is Part Of LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2018.4 urn:nbn:de:0030-drops-91749 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.4 eng https://creativecommons.org/licenses/by/3.0/legalcode