We study the nature of applicative bisimilarity in 𝜆-calculi endowed with operators for sampling from continuous distributions. On the one hand, we show that bisimilarity, logical equivalence, and testing equivalence all coincide with contextual equivalence when real numbers can be manipulated only through continuous functions. The key ingredient towards this result it a novel notion of Feller-continuity for labelled Markov processes, which we believe of independent interest, being a broad class of LMPs for which coinductive and logically inspired equivalences coincide. On the other hand, we show that if no constraint is put on the way real numbers are manipulated, characterizing contextual equivalence turns out to be hard, and most of the aforementioned notions of equivalence are even unsound.
Mon 12 SepDisplayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
10:30 - 12:10 | Lambda Calculus and SemanticsICFP Papers and Events at Linhart Chair(s): Silvia Ghilezan University of Novi Sad, Mathematical Institute SASA | ||
10:30 20mTalk | The Theory of Call-by-Value Solvability ICFP Papers and Events DOI | ||
10:50 20mTalk | A Simple and Efficient Implementation of Strong Call by Need by an Abstract Machine ICFP Papers and Events Malgorzata Biernacka University of Wrocław, Witold Charatonik University of Wrocław, Faculty of Mathematics and Computer Science, Tomasz Drab University of Wrocław, Faculty of Mathematics and Computer Science DOI | ||
11:10 20mTalk | On Feller Continuity and Full Abstraction ICFP Papers and Events Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain, Raphaëlle Crubillé CNRS, Ugo Dal Lago University of Bologna; Inria, Francesco Gavazzo University of Bologna & INRIA Sophia Antipolis DOI | ||
11:30 20mTalk | Multi Types and Reasonable SpaceDistinguished Paper ICFP Papers and Events Beniamino Accattoli Inria & Ecole Polytechnique, Ugo Dal Lago University of Bologna; Inria, Gabriele Vanoni University of Bologna & INRIA Sophia Antipolis DOI | ||
11:50 20mTalk | Denotational semantics as a foundation for cost recurrence extraction for functional languagesJFP Presentation ICFP Papers and Events |