Formalizing Implicative Algebras in Coq - Archive ouverte HAL Access content directly
Conference Papers Year :

Formalizing Implicative Algebras in Coq



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.
Fichier principal
Vignette du fichier
impalg.pdf (413.43 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01703524 , version 1 (07-02-2018)



É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⟩
282 View
378 Download



Gmail Facebook Twitter LinkedIn More