Cited in
(19)- Termination Proofs for Recursive Functions in FoCaLiZe
- Zenon
- EAT
- Coquet
- BWare
- dedukti
- Rocksalt
- Kami
- Meta Dedukti
- Focalide
- CoqInE
- FreeSpec
- operational
- 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
- ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti
- scientific article; zbMATH DE number 7178363 (Why is no real title available?)
This page was built for software: FoCaLiZe
