Detalle del congreso

Autores: Díaz-Caro, Alejandro; Martínez, Guido.

Resumen: Driven by the interest of reasoning about probabilistic programming languages, we set out to study a notionof uniqueness of normal forms for them. To provide a tractable proof method for it, we define a propertyof distribution confluence which is shown to imply the desired uniqueness (even for infinite sequencesof reduction) and further properties. We then carry over several criteria from the classical case, such asNewman?s lemma, to simplify proving confluence in concrete languages. Using these criteria, we obtainsimple proofs of confluence for λ1 , an affine probabilistic λ-calculus, and for Q* , a quantum programminglanguage for which a related property has already been proven in the literature.

Tipo de reunión: Workshop.

Producción: Confluence in Probabilistic Rewriting.

Reunión científica: 12th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2017).

Lugar: Brasilia.

Publicado: No

Mes de reunión: 9

Año: 2017.