Formalizing implicative algebras in Coq

DOI10.1007/978-3-319-94821-8_27MaRDI QIDQ1791188zbMATH OpenOpenAlexFDO

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

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

Recommendations

• Implicative algebras: a new foundation for realizability and forcing
• The category of implicative algebras and realizability
• Developing the algebraic hierarchy with type classes in Coq
• Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
• A constructive algebraic hierarchy in Coq.

Cited in

(10)

• Mac Lane's comparison theorem for the Kleisli construction formalized in Coq
• Towards an algebraic semantics for implicatives
• Algebraic-coalgebraic specification in CoCASL
• scientific article; zbMATH DE number 1670755 (Why is no real title available?)
• scientific article; zbMATH DE number 1070623 (Why is no real title available?)
• Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL
• The category of implicative algebras and realizability
• Implicative algebras: a new foundation for realizability and forcing
• Extending Coq with Imperative Features and Its Application to SAT Verification
• Integration of multiple formal matrix models in Coq

Describes a project that uses

Uses Software

• Coq
• PoplMark

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1791188)