Two type-theoretic approaches to probabilistic termination

Carte non disponible

Date(s) - 21/09/2017
11 h 00 min - 12 h 00 min

Catégories Pas de Catégories

A fundamental result in lambda-calculus states that terms that admit a simple type are strongly normalizing: in other words, they always terminate. The simply-typed lambda-calculus can be enriched with a recursion operator and, in this case, terms admitting a sized type always terminate. In this talk, we study a simply-typed lambda-calculus enhanced with a recursion operator and a probabilistic choice operator, and we focus on the probabilistic counterpart of termination: almost-sure termination (AST), that is, termination with probability 1. I will explain how the sized types approach can be extended to the probabilistic setting, so that we obtain a type system in which typability guarantees AST. I will then sketch ongoing work on a more powerful approach using dependent types, in order to capture AST for a wider class of programs. This is joint work with Dal Lago.

Posts created 14

Articles similaires

Commencez à saisir votre recherche ci-dessus et pressez Entrée pour rechercher. ESC pour annuler.

Retour en haut
Secured By miniOrange