Formalizing Implicative Algebras in Coq

Étienne Miquey 1
1 GALLINETTE - GALLINETTE
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.
Type de document :
Communication dans un congrès
ITP 2018 - 9th International Conference on Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. Springer, 10895, pp.459-476, LNCS. 〈10.1007/978-3-319-94821-8_27〉
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01703524
Contributeur : Étienne Miquey <>
Soumis le : mercredi 7 février 2018 - 23:39:10
Dernière modification le : mercredi 3 octobre 2018 - 11:10:58

Fichier

impalg.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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

Partager

Métriques

Consultations de la notice

235

Téléchargements de fichiers

106