Skip to Main content Skip to Navigation
Conference papers

Formalizing Implicative Algebras in Coq

Étienne Miquey 1
1 GALLINETTE - Gallinette : vers une nouvelle génération d'assistant à la preuve
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
Abstract : We present a Coq formalization of Alexandre Miquel’s implicative algebras, which aim at providing a general algebraic framework for the study of classical realizability models. We first give a self-contained presentation of the underlying implicative structures, which roughly consists of a complete lattice equipped with a binary law representing the implication. We then explain how these structures can beturned into models by adding separators, giving rise to the so-called implicative algebras. Additionally, we show how they generalize Boolean and Heyting algebras as well as the usual algebraic structures used in the analysis of classical realizability.
Document type :
Conference papers
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Étienne Miquey Connect in order to contact the contributor
Submitted on : Wednesday, February 7, 2018 - 11:39:10 PM
Last modification on : Wednesday, November 3, 2021 - 4:23:16 AM


Files produced by the author(s)



Étienne Miquey. Formalizing Implicative Algebras in Coq. ITP 2018 - 9th International Conference on Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. pp.459-476, ⟨10.1007/978-3-319-94821-8_27⟩. ⟨hal-01703524⟩



Les métriques sont temporairement indisponibles