| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 424029 | Electronic Notes in Theoretical Computer Science | 2007 | 22 Pages |
Abstract
We compare several reduction and conversion strategies for the Calculus of (co)Inductive Constructions by running benchmarks from the library of the Coq proof assistant. All the strategies have been implemented in an independent verifier for the proof objects of Coq that is part of the Matita proof assistant.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
