Reduction and Conversion Strategies for the Calculus of (co)Inductive Constructions: Part I |
| |
| Authors: | Claudio Sacerdoti Coen |
| |
| Affiliation: | aDepartment of Computer Science, University of Bologna, Bologna, Italy |
| |
| 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. |
| |
| Keywords: | reduction strategy conversion calculus of inductive construction abstract machine |
| 本文献已被 ScienceDirect 等数据库收录！ |
