The category of implicative algebras and realizability

DOI10.1017/S0960129519000100zbMath1468.03084arXiv1712.06043OpenAlexW2974926966MaRDI QIDQ5108535

Octavio Malherbe, Walter Ricardo Ferrer Santos

Publication date: 4 May 2020

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1712.06043

zbMATH Keywords

realizabilitycombinatory algebrasabstract Krivine's structuresapplicative morphismscomputationally dense morphisms

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topoi (18B25) Combinatory logic and lambda calculus (03B40)

Related Items (1)

Implicative algebras: a new foundation for realizability and forcing

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Realizability. An introduction to its categorical side
• Dependent choice, `quote' and the clock
• The formal theory of monads
• All realizability is relative
• Tripos theory
• Ordered partial combinatory algebras
• Realizability in ordered combinatory algebras with adjunction
• Implicative algebras: a new foundation for realizability and forcing
• Krivine's classical realisability from a categorical perspective
• Iterated realizability as a comma construction
• Classical and Relative Realizability
• Typed lambda-calculus in classical Zermelo-Fraenkel set theory

This page was built for publication: The category of implicative algebras and realizability