Declarative Proof Translation (Short Paper)

DOI10.4230/LIPIcs.ITP.2019.35OpenAlexW2978888779MaRDI QIDQ5875449

Cezary Kaliszyk, Karol Pąk

Publication date: 3 February 2023

Full work available at URL: https://doi.org/10.4230/LIPIcs.ITP.2019.35

zbMATH Keywords

translationMizardeclarative proofIsabelle/Isar

Mathematics Subject Classification ID

Related Items

Combining higher-order logic with set theory formalizations

Uses Software

• Coq
• Isar
• Mizar
• Lean
• miz3

Cites Work

• Unnamed Item
• Four decades of {\textsc{Mizar}}. Foreword
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Isabelle import infrastructure for the Mizar Mathematical Library
• A comparison of Mizar and Isar
• Semantics of Mizar as an Isabelle object logic
• A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
• The Lean Theorem Prover (System Description)
• A Declarative Language for the Coq Proof Assistant
• Proof Auditing Formalised Mathematics