Étienne Miquey
LIP, ÉNS Lyon
http://perso.ens-lyon.fr/etienne.miquey/
Date(s) : 15/04/2021 iCal
10 h 30 min - 11 h 30 min
Constructive foundations have for decades been built upon realizability models for higher-order logic and type theory. However, traditional realizability models have a rather limited notion of computation, which only supports non-termination and avoids many other commonly used effects. Work to address these limitations has typically overlaid structure on top of existing models, such as by using powersets to represent non-determinism, but kept the realizers themselves deterministic. On the other hand, the algebraic structure of existing realizability models taking into account effects in a more direct fashion (as is done in Krivine realizability for instance) is hard to analyze.
In this work, we (Liron Cohen, Ross Tate & myself) alternatively address these limitations by making the structure underlying realizability models more flexible. To this end, we introduce evidenced frames: a general-purpose framework for building realizability models that support diverse effectful computations. We demonstrate that this flexibility permits models wherein the realizers themselves can be effectful, such as λ-terms that can manipulate state, reduce non-deterministically, or fail entirely. Beyond the broader notions of computation, we demonstrate that evidenced frames form a unifying framework for (realizability) models of higher-order dependent predicate logic. In particular, we prove that evidenced frames are complete with respect to these models, and that the existing completeness construction for implicative algebras—another foundational framework for realizability—factors through our simpler construction. As such, we conclude that evidenced frames offer an ideal domain for unifying and broadening realizability models.
http://perso.ens-lyon.fr/etienne.miquey/content/lics21-ef.pdf
Catégories