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:7679@i2m.univ-amu.fr DTSTART;TZID=Europe/Paris:20161208T140000 DTEND;TZID=Europe/Paris:20161208T160000 DTSTAMP:20241210T072539Z URL:https://www.i2m.univ-amu.fr/evenements/lambda-theories-probabilistes/ SUMMARY:Thomas Leventis (I2M\, Aix-Marseille université): Lambda-théories probabilistes DESCRIPTION:Thomas Leventis: Le lambda-calcul est un formalisation de la no tion de calcul. Dans cette thèse nous nous intéresserons à certaines va riantes non déterministes\, et nous nous pencherons plus particulièremen t sur le cas probabiliste.\nL'étude du lambda-calcul probabiliste n'est p as nouvelle\, mais les travaus précédents considéraient le comportement probabiliste comme un effet de bord. Notre objectif est de présenter ce calcul d'une manière plus équationnelle\, en intégrant le comportement probabiliste à la réduction.\nTout d'abord nous définissons une sémant ique opérationnelle déterministe et contextuelle pour le lambda-calcul p robabiliste en appel par nom. Afin de traduire la signification de la somm e nous définissons une équivalence synaxique dans notre calcul\, dont no us démontrons qu'il ne déforme pas la réduction: considérer une réduc tion modulo équivalence revient à considérer simplement le résultat du calcul modulo équivalence. Nous prouvons également un résultat de stan dardisation.\nDans ce cadre nous définissons une notion de théorie équa tionnelle pour le lambda-calcul probabiliste. Nous étendons certaines not ions usuelles\, et en particulier celle de bon sens. Cette dernière se fo rmalise facilement dans un cadre déterministe mais est bien plus complexe dans le cas probabiliste.\nPour finir nous prouvons une correspondance en tre l'équivalence observationnelle\, l'égalité des arbres de Böhm et l a théorie cohérente sensée maximale. Nous définissons une notion d'arb res de Böhm probabilistes dont nous prouvons qu'elle forme un modèle. No us démontrons ensuite un résultat de séparabilité disant que deux term es avec des arbres de Böhm distincts ne sont pas observationnellement éq uivalents.\n[su_spacer size="10"]Résumé en anglais :\nThe lambda-calculu s is a way to formalize the notion of computation. In this thesis we will be interested in some of these variants introducing non deterministim\, an d we will focus mostly on a probabilistic calculus.\nThe probabilistic lam bda-calculus has been studied for some time\, but the probabilistic behavi our has always been treated as a side effect. Our purpose is to give a mor e equational representation of this calculus\, by handling the probabiliti es inside the reduction rather than as a side effect.\nTo begin with we gi ve a deterministic and contextual operational semantics for the call-by-na me probabilistic lambda-calculus. To express the probabilistic behaviour o f the sum we introduce a syntactic equivalence in our calculus\, and we sh ow it has little consequence on the calculus: reducing modulo equivalence amount to reducing and then looking at the result modulo equivalence. We a lso prove a standardization theorem.\nThen using this operational semantic s we define a notion of equational theories for the probabilistic lambda-c alculus. We extend some usual notions to this setting\, and in particular the sensibility of a theory. This notion is quite simple in a deterministi c setting but becomes more complicated when we have a probabilistic comput ation.\nFinally we prove a generalization of the equality between the obse rvational equivalence\, the Böhm tree equality and the maximal coherent s ensible lambda-theory. We give a notion of probabilistic Böhm trees\, and prove that this forms a model of the probabilistic lambda-calculus. Then we prove a separability result stating that two terms with different Böhm trees are separable\, i.e. are not observationally equivalent.\n-\nMembre s du jury :-\n- Antonino SALIBRA\, Université de Venise Ca'Foscari (Rappo rteur)\n- Delia KESNER\, Université Paris Diderot (Examinateur)\n- Ugo DA L LAGO\, Université de Bologne (Examinateur)\n- Michele PAGANI\, Universi té Paris Diderot (Examinateur)\n- Lionel VAUX\, Aix-Marseille Université (Directeur de thèse)\n- Laurent REGNIER\, Aix-Marseille Université (Co- directeur de thèse)\n-\n-\nLien : theses.fr ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2 015/06/Thomas_Leventis.jpg CATEGORIES:Soutenance de thèse,AGLR,Logique et Interactions END:VEVENT BEGIN:VTIMEZONE TZID:Europe/Paris X-LIC-LOCATION:Europe/Paris BEGIN:STANDARD DTSTART:20161030T020000 TZOFFSETFROM:+0200 TZOFFSETTO:+0100 TZNAME:CET END:STANDARD END:VTIMEZONE END:VCALENDAR