Realizability. An introduction to its categorical side

Publication date: 8 April 2009

Published in: Studies in Logic and the Foundations of Mathematics (Search for Journal in Brave)

zbMATH Keywords

arithmetic set theory partial combinatory algebra effective topos assemblies synthetic domain theory realizability topos partial recursive functions geometric morphism axiomatic computability theory tripos

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Categorical logic, topoi (03G30) Topoi (18B25) Recursive functions and relations, subrecursive hierarchies (03D20) Other constructive mathematics (03F65) Intuitionistic mathematics (03F55)

Related Items

Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model, The intrinsic topology of Martin-Löf universes, The effects of effects on constructivism, On Church’s thesis in cubical assemblies, Converse extensionality and apartness, CZF does not have the existence property, Axiomatic reals and certified efficient exact real computation, Partial combinatory algebra and generalized numberings, Dialectica logical principles, On a generalization of equilogical spaces, Semantics of higher-order quantum computation via geometry of interaction, A topos for continuous logic, Realizability Models Separating Various Fan Theorems, Triposes as a generalization of localic geometric morphisms, Quotient completion for the foundation of constructive mathematics, Natural factors of the Muchnik lattice capturing IPC, Relating first-order set theories, toposes and categories of classes, Basic subtoposes of the effective topos, Functoriality of modified realizability, Sheaves of structures, Heyting‐valued structures, and a generalization of Łoś's theorem, EXTENSIONAL REALIZABILITY AND CHOICE FOR DEPENDENT TYPES IN INTUITIONISTIC SET THEORY, Choice and independence of premise rules in intuitionistic set theory, The category of implicative algebras and realizability, First-order logic in the Medvedev lattice, A characterization of generalized existential completions, Stateful Realizers for Nonstandard Analysis, On categorical structures arising from implicative algebras: from topology to assemblies, A constructive picture of Noetherian conditions and well quasi-orders, Nonstandard proof methods in toposes, On the failure of fixed-point theorems for chain-complete lattices in the effective topos, Embeddings between partial combinatory algebras, What should a generic object be?, Parallelism in realizability models, Ordered combinatory algebras and realizability, Categories of partial equivalence relations as localizations, Constructive toposes with countable sums as models of constructive set theory, Characterizing partitioned assemblies and realizability toposes, A characterization of those categories whose internal logic is Hilbert's \(\varepsilon\)-calculus, The number of countable models in realizability toposes, Realizability in ordered combinatory algebras with adjunction, On the Semantics of Intensionality, On Choice Rules in Dependent Type Theory, Implicative algebras: a new foundation for realizability and forcing, Triposes, q-toposes and toposes, Natural factors of the Medvedev lattice capturing IPC, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting), Regular functors and relative realisability categories, Some reasons for generalising domain theory, Univalent polymorphism, On (co)products of partial combinatory algebras, with an application to pushouts of realizability toposes, A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS, Krivine's classical realisability from a categorical perspective, Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice, Realizability with a local operator of A. M. Pitts, A co-free construction for elementary doctrines, Unifying exact completions, Categorical simulations, Aspects of predicative algebraic set theory. II: Realizability, REALIZABILITY SEMANTICS FOR QUANTIFIED MODAL LOGIC: GENERALIZING FLAGG’S 1985 CONSTRUCTION, Computability structures, simulations and realizability, A notion of homotopy for the effective topos, An injection from the Baire space to natural numbers, Kripke models for subtheories of \textsf{CZF}, Realizability models refuting Ishihara's boundedness principle, Unnamed Item, Every metric space is separable in function realizability, Unnamed Item, The Herbrand topos, The Herbrand topos, SEPARATING THE FAN THEOREM AND ITS WEAKENINGS II, Monoidal computer III: a coalgebraic view of computability and complexity (extended abstract), On the Failure of Fixed-Point Theorems for Chain-complete Lattices in the Effective Topos, Unnamed Item, Fixed point theorems for precomplete numberings, COMPUTABILITY IN PARTIAL COMBINATORY ALGEBRAS, A game-semantic model of computation, On the Bourbaki–Witt principle in toposes, Exploring mathematical objects from custom-tailored mathematical universes, A categorical reading of the numerical existence property in constructive foundations, A homotopy-theoretic model of function extensionality in the effective topos, LIFSCHITZ REALIZABILITY AS A TOPOLOGICAL CONSTRUCTION, Aspects of Categorical Recursion Theory, ORDINAL ANALYSIS OF PARTIAL COMBINATORY ALGEBRAS, Models of intuitionistic set theory in subtoposes of nested realizability toposes, Maximal ideals in countable rings, constructively, Third-order functionals on partial combinatory algebras, Computability of Subsets of Metric Spaces, Bishop-Style Constructive Reverse Mathematics, Lawvere-Tierney topologies for computability theorists