Krivine's classical realisability from a categorical perspective

DOI10.1017/S0960129512000989zbMath1326.03083MaRDI QIDQ5410238

Thomas Streicher

Publication date: 16 April 2014

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

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55) Combinatory logic and lambda calculus (03B40)

Related Items (7)

The category of implicative algebras and realizability ⋮ On categorical structures arising from implicative algebras: from topology to assemblies ⋮ A correspondence between maximal abelian sub-algebras and linear logic fragments ⋮ Ordered combinatory algebras and realizability ⋮ Realizability in ordered combinatory algebras with adjunction ⋮ Implicative algebras: a new foundation for realizability and forcing ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)

Cites Work

• Unnamed Item
• Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation)
• Realizability. An introduction to its categorical side
• Dependent choice, `quote' and the clock
• All realizability is relative
• Classical logic, continuation semantics and abstract machines
• Ordered partial combinatory algebras
• Typed lambda-calculus in classical Zermelo-Fraenkel set theory

This page was built for publication: Krivine's classical realisability from a categorical perspective