Implicative algebras: a new foundation for realizability and forcing
From MaRDI portal
Publication:5139288
DOI10.1017/S0960129520000079zbMath1498.03043arXiv1802.00528MaRDI QIDQ5139288
Publication date: 8 December 2020
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1802.00528
Categorical logic, topoi (03G30) Proof theory in general (including proof-theoretic semantics) (03F03) Semilattices (06A12) Combinatory logic and lambda calculus (03B40) Other aspects of forcing and Boolean-valued models (03E40) Abstract algebraic logic (03G27)
Related Items
Triposes as a generalization of localic geometric morphisms ⋮ The category of implicative algebras and realizability ⋮ Stateful Realizers for Nonstandard Analysis ⋮ On categorical structures arising from implicative algebras: from topology to assemblies ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Linear logic
- Principal type schemes for an extended type theory
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Realizability. An introduction to its categorical side
- Minimally generated Boolean algebras
- Dependent choice, `quote' and the clock
- Realizability algebras II : new models of ZF + DC
- Specifying Peirce's law in classical realizability
- Ordered combinatory algebras and realizability
- Existential witness extraction in classical realizability and via a negative translation
- Tripos theory in retrospect
- Realizability algebras: a program to well order R
- A filter lambda model and the completeness of type assignment
- Proofs of strong normalisation for second order classical natural deduction
- The category of implicative algebras and realizability
- Krivine's classical realisability from a categorical perspective
- Intensional interpretations of functionals of finite type I
- THE INDEPENDENCE OF THE CONTINUUM HYPOTHESIS
- On the interpretation of intuitionistic number theory
- Realizability: a historical essay
- Typed lambda-calculus in classical Zermelo-Fraenkel set theory