Formalizing implicative algebras in Coq

DOI10.1007/978-3-319-94821-8_27OpenAlexW2786761800MaRDI QIDQ1791188

Étienne Miquey

Publication date: 4 October 2018

Full work available at URL: https://hal.inria.fr/hal-01703524/file/impalg.pdf

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20) Abstract algebraic logic (03G27)

Uses Software

• Coq
• PoplMark

This page was built for publication: Formalizing implicative algebras in Coq