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:8985@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20260212T110000
DTEND;TZID=Europe/Paris:20260212T123000
DTSTAMP:20260205T180853Z
URL:https://www.i2m.univ-amu.fr/evenements/is-typed-realizability-only-pre
 dicative/
SUMMARY:Félix Castro (I2M\, Aix-Marseille): Is typed realizability only pr
 edicative?
DESCRIPTION:Félix Castro: In Kleene realizability\, formulas are interpret
 ed as sets of\n(untyped) programs. This approach allows for a sound interp
 retation of\nHigher-Order Logic (HOL): it leads to the definition of the e
 ffective\ntopos and\, more generally\, to a wide range of toposes obtained
  from\n"partial combinatory algebras". All these realizability toposes hav
 e\nan important common feature: they arise from an untyped model of\ncompu
 tations.\n\nOn the other hand\, typed programming languages were also used
  to\ndesign realizability models. Notably\, Paulin-Mohring extended Kreise
 l\nmodified realizability to the Calculus of Constructions (CC)\, thus\ngi
 ving a typed realizability interpretation of HOL. It is therefore\nnatural
  to ask whether one can build toposes from such typed\ninterpretations. Un
 fortunately\, the answer is negative: Lietz and\nStreicher showed that the
  (Set-based) categorical models coming from a\n"typed partial combinatory 
 algebra" are impredicative only if it is\nessentially untyped.\n\nIt seems
  unsatisfactory to me: if a typed programming language is\nstrong enough t
 o interpret HOL\, it should be possible to obtain\ndirectly an impredicati
 ve categorical model from it! During this talk\,\nwe will work internally 
 in an extension of CC to build an "evidenced\nframe" from (a variation of)
  Paulin-Mohring model and without\ndegenerating the type system of the cal
 culus at stake. Because\ntriposes can be built from evidenced frames\, thi
 s work is a first step\ntoward an answer of the title question: no\, typed
  realizability is not\nonly (categorically) predicative!
CATEGORIES:Séminaire,Logique et Interactions
LOCATION:I2M Luminy - TPR2\, Salle de Séminaire 304-306 (3ème étage)\, 1
 63 Avenue de Luminy\, Marseille\, 13009\, France
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=163 Avenue de Luminy\, Mars
 eille\, 13009\, France;X-APPLE-RADIUS=100;X-TITLE=I2M Luminy - TPR2\, Sall
 e de Séminaire 304-306 (3ème étage):geo:0,0
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20251026T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR