Linear Realisability and Implicative Algebras

Alexandre Lucquin, Luc Pellissier, Thomas Seiller

Realizability, introduced by Kleene, can be understood as a concretization of the Brouwer-Heyting-Kolmogorov (BHK) interpretation of proofs, providing a framework to interpret math…