Towards automatic transformations of Coq proof scripts

DOI10.4204/EPTCS.398.4MaRDI QIDQ6934150zbMATH OpenFDO

Authors Nicolas Magaud

Publication date 3 September 2025

Full work available at URL https://doi.org/10.4204/EPTCS.398.4

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• scientific article; zbMATH DE number 1696760 (Why is no real title available?)
• An introduction to small scale reflection in Coq
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Mechanical Theorem Proving in Tarski’s Geometry
• Mechanization of incidence projective geometry in higher dimensions, a combinatorial approach
• Mtac: a monad for typed tactic programming in Coq
• Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
• Two new ways to formally prove Dandelin-Gallucci's theorem

This page was built for publication: Towards automatic transformations of Coq proof scripts

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