@InProceedings{sakaguchi:LIPIcs.ITP.2022.29, author = {Sakaguchi, Kazuhiko}, title = {{Reflexive Tactics for Algebra, Revisited}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {29:1--29:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-252-5}, ISSN = {1868-8969}, year = {2022}, volume = {237}, editor = {Andronick, June and de Moura, Leonardo}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.29}, URN = {urn:nbn:de:0030-drops-167385}, doi = {10.4230/LIPIcs.ITP.2022.29}, annote = {Keywords: Coq, Elpi, \lambdaProlog, Mathematical Components, algebraic structures, packed classes, canonical structures, proof by reflection} }