FoCaLiZe

MaRDI QIDQ24313swMATHFDO

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

Described by source

• FoCaLiZe and Dedukti to the rescue for proof interoperability

Cited in

(19)

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

This page was built for software: FoCaLiZe