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:7651@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20170126T110000
DTEND;TZID=Europe/Paris:20170126T120000
DTSTAMP:20241120T204747Z
URL:https://www.i2m.univ-amu.fr/evenements/deciding-simply-typed-equivalen
 ce-with-sums-and-the-empty-type-2/
SUMMARY:Gabriel Scherer (Parsifal team at INRIA Saclay): Deciding simply-ty
 ped equivalence with sums and the empty type
DESCRIPTION:Gabriel Scherer: The simply-typed λ-calculus\, with only funct
 ion types\, is strongly normalizing\, and its program equivalence relation
  is decidable: unlike in more advanced type system with polymorphism or ef
 fects\, the natural "syntactic" equivalence (βη-equivalence) corresponds
  to natural "semantic" equivalence (observational or contextual equivalenc
 e)\, and is decidable. Adding product types (pairs) is easy and preserves 
 these properties\, but sums (disjoint unions) are\, surprisingly\, harder.
  It is only in 1995 that Neil Ghani proved that the equivalence in presenc
 e of sums is decidable\, and the situation in presence of the empty type (
 zero-ary sum) was unknown.\nWe propose an equivalence algorithm for sums a
 nd the empty type that takes inspiration from a proof-theoretic technique\
 , named "focusing"\,designed for proof search. The exposition will be intr
 oductory\; I will present the difficulties caused by sums and the empty ty
 pe\, present some of the existing approaches for sums in the literature\, 
 introduce focusing\, and give a high-level intuition of our saturation-bas
 ed algorithm and its termination argument.\n\n\n
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Gabriel_Scherer.jpg
CATEGORIES:Séminaire,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