Cited in
(10)- Verified heap theorem prover by paramodulation
- Residual theory in λ-calculus: a formal development
- Inductive families
- VeriStar
- VeriSmall
- Mtac
- VeriML
- Extensible and efficient automation through reflective tactics
- Towards certified meta-programming with typed Template-Coq
- scientific article; zbMATH DE number 1070623 (Why is no real title available?)
This page was built for software: Gallina
