FoCaLiZe

swMATH12384MaRDI QIDQ24313FDOQ24313

Author name not available (Why is that?)

Described by source

• FoCaLiZe and Dedukti to the rescue for proof interoperability

Cited In (7)

• Termination Proofs for Recursive Functions in FoCaLiZe
• ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti
• Tactics and certificates in Meta Dedukti
• Theories as types
• Modular verification of programs with effects and effects handlers
• Modelling algebraic structures and morphisms in ACL2
• Title not available (Why is that?)

This page was built for software: FoCaLiZe