Environmental Bisimulations for Probabilistic Higher-order Languages
| Autor: | Valeria Vignudelli, Davide Sangiorgi |
|---|---|
| Přispěvatelé: | Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), Foundations of Component-based Ubiquitous Systems (FOCUS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Dipartimento di Informatica - Scienza e Ingegneria [Bologna] (DISI), Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO)-Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), ANR-12-IS02-0001,PACE,Processus non-standard: Analyse, Coinduction, Expressivité(2012), R. Bodik, R. Majumdar, Sangiorgi, Davide, Vignudelli, Valeria, Sangiorgi D., Vignudelli V. |
| Rok vydání: | 2019 |
| Předmět: |
TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES
Theoretical computer science Computer science Imperative Languages Environmental Bisimulation 0102 computer and information sciences 02 engineering and technology Mathematical proof 01 natural sciences [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] Congruence (geometry) Contextual Equivalence 0202 electrical engineering electronic engineering information engineering [INFO]Computer Science [cs] Equivalence (formal languages) Equivalence (measure theory) Abstraction (linguistics) [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Probabilistic logic Preorder [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Contrast (statistics) 020207 software engineering Imperative language Computer Graphics and Computer-Aided Design Probabilistic Lambda Calculus TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Imperative programming 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Higher order languages Algorithm Software |
| Zdroj: | POPL '16 POPL '16, Jan 2016, St. Petersburg, United States. ⟨10.1145/2837614.2837651⟩ POPL |
| ISSN: | 1558-4593 0164-0925 |
| DOI: | 10.1145/3350618 |
| Popis: | Environmental bisimulations for probabilistic higher-order languages are studied. In contrast with applicative bisimulations, environmental bisimulations are known to be more robust and do not require sophisticated techniques such as Howe’s in the proofs of congruence. As representative calculi, call-by-name and call-by-value λ-calculus, and a (call-by-value) λ-calculus extended with references (i.e., a store) are considered. In each case, full abstraction results are derived for probabilistic environmental similarity and bisimilarity with respect to contextual preorder and contextual equivalence, respectively. Some possible enhancements of the (bi)simulations, as “up-to techniques,” are also presented. Probabilities force a number of modifications to the definition of environmental bisimulations in non-probabilistic languages. Some of these modifications are specific to probabilities, others may be seen as general refinements of environmental bisimulations, applicable also to non-probabilistic languages. Several examples are presented, to illustrate the modifications and the differences. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|