Skip to Main content Skip to Navigation
New interface
Conference papers

Evidenced Frames: A Unifying Framework Broadening Realizability Models

Abstract : 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. This paper alternatively addresses 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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03422961
Contributor : Etienne Miquey Connect in order to contact the contributor
Submitted on : Tuesday, November 9, 2021 - 6:16:22 PM
Last modification on : Thursday, September 29, 2022 - 2:58:07 PM
Long-term archiving on: : Thursday, February 10, 2022 - 7:54:46 PM

File

LICS21-EF.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03422961, version 1

Collections

Citation

Liron Cohen, Étienne Miquey, Ross Tate. Evidenced Frames: A Unifying Framework Broadening Realizability Models. LICS 2021, Jul 2021, Rome, Italy. ⟨hal-03422961⟩

Share

Metrics

Record views

98

Files downloads

165