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:6449@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20210415T103000
DTEND;TZID=Europe/Paris:20210415T113000
DTSTAMP:20241120T201436Z
URL:https://www.i2m.univ-amu.fr/evenements/evidenced-frames-a-unifying-fra
 mework-broadening-realizability-models/
SUMMARY:Étienne Miquey (LIP\, ÉNS Lyon): Evidenced frames: a unifying fra
 mework broadening realizability models
DESCRIPTION:Étienne Miquey: Constructive foundations have for decades been
  built upon realizability models for higher-order logic and type theory. H
 owever\, traditional realizability models have a rather limited notion of 
 computation\, which only supports non-termination and avoids many other co
 mmonly used effects. Work to address these limitations has typically overl
 aid structure on top of existing models\, such as by using powersets to re
 present non-determinism\, but kept the realizers themselves deterministic.
  On the other hand\, the algebraic structure of existing realizability mod
 els taking into account effects in a more direct fashion (as is done in Kr
 ivine realizability for instance) is hard to analyze.\n\nIn this work\, we
  (Liron Cohen\, Ross Tate &amp\; myself) alternatively address these limit
 ations by making the structure underlying realizability models more flexib
 le. To this end\, we introduce evidenced frames: a general-purpose framewo
 rk for building realizability models that support diverse effectful comput
 ations. We demonstrate that this flexibility permits models wherein the re
 alizers themselves can be effectful\, such as λ-terms that can manipulate
  state\, reduce non-deterministically\, or fail entirely. Beyond the broad
 er notions of computation\, we demonstrate that evidenced frames form a un
 ifying framework for (realizability) models of higher-order dependent pred
 icate logic. In particular\, we prove that evidenced frames are complete w
 ith respect to these models\, and that the existing completeness construct
 ion for implicative algebras—another foundational framework for realizab
 ility—factors through our simpler construction. As such\, we conclude th
 at evidenced frames offer an ideal domain for unifying and broadening real
 izability models.\nhttp://perso.ens-lyon.fr/etienne.miquey/content/lics21-
 ef.pdf\n\n&nbsp\;
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 015/07/Etienne_Miquey.jpg
CATEGORIES:Séminaire,Logique et Interactions,Virtual event
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:20210328T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR