Steven Schäfer, Gert Smolka, Tobias Tebbi. Completeness and Decidability of de Bruijn Substitution Algebra in Coq. In Xavier Leroy, Alwen Tiu, editors, Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015. pages 67-73, ACM, 2015. [doi]
@inproceedings{SchaferST15,
title = {Completeness and Decidability of de Bruijn Substitution Algebra in Coq},
author = {Steven Schäfer and Gert Smolka and Tobias Tebbi},
year = {2015},
doi = {10.1145/2676724.2693163},
url = {http://doi.acm.org/10.1145/2676724.2693163},
researchr = {https://researchr.org/publication/SchaferST15},
cites = {0},
citedby = {0},
pages = {67-73},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015},
editor = {Xavier Leroy and Alwen Tiu},
publisher = {ACM},
isbn = {978-1-4503-3296-5},
}