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

Author Valeria Vignudelli

Thumbnail PDF


  • Filesize: 207 kB
  • 2 pages

Document Identifiers

Author Details

Valeria Vignudelli
  • Univ Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP, Lyon, France

Cite AsGet BibTex

Valeria Vignudelli. Proof Techniques for Program Equivalence in Probabilistic Higher-Order Languages (Invited Talk). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


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].

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Operational semantics
  • Theory of computation → Probabilistic computation
  • Lambda Calculus
  • Contextual Equivalence
  • Bisimulation
  • Probabilistic Programming Languages


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Samson Abramsky. The lazy lambda calculus. In David A. Turner, editor, Research topics in functional programming, pages 65-116. Addison-Wesley, 1990. Google Scholar
  2. Ales Bizjak and Lars Birkedal. Step-indexed logical relations for probability. In Proc. FoSSaCS'15, pages 279-294, 2015. Google Scholar
  3. Raphaëlle Crubillé and Ugo Dal Lago. On probabilistic applicative bisimulation and call-by-value λ-calculi. In Proc. ESOP'14, LNCS 8410, pages 209-228. Springer, 2014. URL:
  4. Raphaëlle Crubillé, Ugo Dal Lago, Davide Sangiorgi, and Valeria Vignudelli. On applicative similarity, sequentiality, and full abstraction. In Roland Meyer, André Platzer, and Heike Wehrheim, editors, Correct System Design, LNCS 9360, pages 65-82. Springer, 2015. Google Scholar
  5. Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti. On coinductive equivalences for higher-order probabilistic functional programs. In Proc. POPL'14, pages 297-308. ACM, 2014. Google Scholar
  6. James H. Morris. Lambda-calculus models of programming languages. PhD thesis, Massachusetts Institute of Technology., 1968. Google Scholar
  7. Andrew Pitts. Typed operational reasoning. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 7, pages 245-289. MIT Press, 2005. Google Scholar
  8. Davide Sangiorgi and Valeria Vignudelli. Environmental bisimulations for probabilistic higher-order languages. In Proc. POPL'16, pages 595-607. ACM, 2016. Google Scholar