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:7877@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20160303T110000
DTEND;TZID=Europe/Paris:20160303T120000
DTSTAMP:20241120T205557Z
URL:https://www.i2m.univ-amu.fr/evenements/dpao-a-dependently-typed-classi
 cal-arithmetic-in-finite-types-which-proves-dependent-choices/
SUMMARY:Hugo Herbelin (INRIA\, Rocquencourt-Paris): dPAω: a dependently-ty
 ped classical arithmetic in finite types which proves dependent choices
DESCRIPTION:Hugo Herbelin: We extend classical arithmetic in finite types w
 ith an intuitionistically-restricted form of strong projection of existent
 ial quantification. In this system\, by turning countable universal quanti
 fication into an infinite tuple\, we can give a proof of the axiom of depe
 ndent choices.\nAll constructions of the system are computational\, hence 
 providing with a proof-as-program interpretation of dPAω. The presence of
  infinite tuples requires however to rely on a lazy evaluation strategy.\n
 \n\n
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Hugo_Herbelin.jpg
CATEGORIES:Séminaire,Logique et Interactions
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20151025T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR