Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Luis Sacchini. A New Elimination Rule for the Calculus of Inductive Constructions. In Stefano Berardi, Ferruccio Damiani, Ugo de Liguoro, editors, Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected Papers. Volume 5497 of Lecture Notes in Computer Science, pages 32-48, Springer, 2008. [doi]
@inproceedings{BarrasCGHS08,
title = {A New Elimination Rule for the Calculus of Inductive Constructions},
author = {Bruno Barras and Pierre Corbineau and Benjamin Grégoire and Hugo Herbelin and Jorge Luis Sacchini},
year = {2008},
doi = {10.1007/978-3-642-02444-3_3},
url = {http://dx.doi.org/10.1007/978-3-642-02444-3_3},
tags = {rule-based, rules},
researchr = {https://researchr.org/publication/BarrasCGHS08},
cites = {0},
citedby = {0},
pages = {32-48},
booktitle = {Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected Papers},
editor = {Stefano Berardi and Ferruccio Damiani and Ugo de Liguoro},
volume = {5497},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
isbn = {978-3-642-02443-6},
}