FoCaLiZe

MaRDI QIDQ24313swMATHFDO

Official website http://focalize.inria.fr/

Described by source

• FoCaLiZe and Dedukti to the rescue for proof interoperability

Cited in

(19)

• Tactics and certificates in Meta Dedukti
• Theories as types
• Zenon
• Modular verification of programs with effects and effects handlers
• EAT
• Coquet
• BWare
• Modelling algebraic structures and morphisms in ACL2
• dedukti
• Termination Proofs for Recursive Functions in FoCaLiZe
• ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti
• Rocksalt
• Kami
• Meta Dedukti
• Focalide
• CoqInE
• scientific article; zbMATH DE number 7178363 (Why is no real title available?)
• operational
• FreeSpec

This page was built for software: FoCaLiZe