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 metadatas

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-01703524
Contributor : Étienne Miquey <>
Submitted on : Wednesday, February 7, 2018 - 11:39:10 PM
Last modification on : Tuesday, March 26, 2019 - 9:25:22 AM

File

impalg.pdf
Files produced by the author(s)

Identifiers

Citation

É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⟩

Share

Metrics

Record views

340

Files downloads

267