FoCaLiZe

swMATH12384MaRDI QIDQ24313FDOQ24313

Author name not available (Why is that?)

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
• Zenon
• EAT
• Coquet
• BWare
• dedukti
• Tactics and certificates in Meta Dedukti
• Rocksalt
• Kami
• Meta Dedukti
• Focalide
• CoqInE
• Theories as types
• FreeSpec
• operational
• Modular verification of programs with effects and effects handlers
• Modelling algebraic structures and morphisms in ACL2
• Title not available (Why is that?)
• ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti

This page was built for software: FoCaLiZe