BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//wp-events-plugin.com//7.2.3.1//EN
TZID:Europe/Paris
X-WR-TIMEZONE:Europe/Paris
BEGIN:VEVENT
UID:7495@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20170921T110000
DTEND;TZID=Europe/Paris:20170921T120000
DTSTAMP:20241120T204347Z
URL:https://www.i2m.univ-amu.fr/evenements/two-type-theoretic-approaches-t
 o-probabilistic-termination/
SUMMARY:Charles Grellois (INRIA Sophia-Antipolis ): Two type-theoretic appr
 oaches to probabilistic termination
DESCRIPTION:Charles Grellois: A fundamental result in lambda-calculus state
 s that terms that admit a simple type are strongly normalizing: in other w
 ords\, they always terminate. The simply-typed lambda-calculus can be enri
 ched with a recursion operator and\, in this case\, terms admitting a size
 d type always terminate. In this talk\, we study a simply-typed lambda-cal
 culus enhanced with a recursion operator and a probabilistic choice operat
 or\, 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 A
 ST. I will then sketch ongoing work on a more powerful approach using depe
 ndent types\, in order to capture AST for a wider class of programs. This 
 is joint work with Dal Lago.\n\n\n
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Charles_Grellois.jpg
CATEGORIES:Séminaire,Logique et Interactions
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:20170326T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR