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:8223@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20141205T103000
DTEND;TZID=Europe/Paris:20141205T120000
DTSTAMP:20241210T144851Z
URL:https://www.i2m.univ-amu.fr/evenements/on-operational-properties-of-qu
 antitative-extensions-of-lambda-calculus/
SUMMARY:Michele Alberti (I2M\, Aix-Marseille Université): On operational p
 roperties of quantitative extensions of lambda-calculus
DESCRIPTION:Michele Alberti: http://www.theses.fr/s119485\n\nIn this thesis
  we deal with the operational behaviours of two quantitative extensions of
  pure λ-calculus\, namely the algebraic λ-calculus and the probabilistic
  λ-calculus.\n\nIn the first part\, we study the β-reduction theory of t
 he algebraic λ-calculus\, a calculus allowing formal finite linear combin
 ations of λ-terms to be expressed. Although the system enjoys the Church-
 Rosser property\, reduction collapses in presence of negative coefficients
 . We exhibit a solution to the consequent loss of the notion of (unique) n
 ormal form\, allowing the definition of a partial\, but consistent\, term 
 equivalence. We then introduce a variant of β-reduction defined on canoni
 cal terms only\, which we show partially characterises the previously esta
 blished notion of normal form. In the process\, we prove a factorisation t
 heorem.\n\nIn the second part\, we study bisimulation and context equivale
 nce in a λ-calculus endowed with a probabilistic choice. We show a techni
 que for proving congruence of probabilistic applicative bisimilarity. Whil
 e the technique follows Howe’s method\, some of the technicalities are q
 uite different\, relying on non-trivial “disentangling” properties for
  sets of real numbers. Finally we show that\, while bisimilarity is in gen
 eral strictly finer than context equivalence\, coincidence between the two
  relations is achieved on pure λ-terms. The resulting equality is that in
 duced by Lévy-Longo trees\, generally accepted as the finest extensional 
 equivalence on pure λ-terms under a lazy regime.\n\n*Membres du jury :\n-
 \n- Simona Ronchi Della Rocca\n- Paul Levy (rapporteur)\n- Michele Pagani 
 (rapporteur)\n- Laurent Regnier (directeur de thèse)\n- Simone Martini (c
 o-directrice de thèse)\n- Emmanuel Beffara\n- Lionel Vaux\n- Ugo Dal Lago
 \n\nLien : theses.fr
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Michele_Alberti.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:20141026T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR