FoCaLiZe and Dedukti to the rescue for proof interoperability

DOI10.1007/978-3-319-66107-0_9zbMath1482.68268OpenAlexW2748296057MaRDI QIDQ1687726

Raphaël Cauderlier, Catherine Dubois

Publication date: 4 January 2018

Full work available at URL: https://hal.inria.fr/hal-01592243/file/article%20%281%29.pdf

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

FoCaLiZe

Uses Software

• Coq
• Isabelle
• HOL
• HOL Light
• Nuprl
• dedukti

Cites Work

• Unnamed Item
• Representing model theory in a type-theoretical logical framework
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• Automatic Proof and Disproof in Isabelle/HOL
• ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti
• Proceedings Fourth Workshop on Proof eXchange for Theorem Proving
• Experimenting with Deduction Modulo
• Scalable LCF-Style Proof Translation
• An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf
• Matching Concepts across HOL Libraries
• Importing HOL Light into Coq

This page was built for publication: FoCaLiZe and Dedukti to the rescue for proof interoperability