Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Thiago Felicissimo and Théo Winterhalter. Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{felicissimo_et_al:LIPIcs.FSCD.2024.21, author = {Felicissimo, Thiago and Winterhalter, Th\'{e}o}, title = {{Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {21:1--21:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.21}, URN = {urn:nbn:de:0030-drops-203503}, doi = {10.4230/LIPIcs.FSCD.2024.21}, annote = {Keywords: Dedukti, Rewriting, Confluence, Dependent types, Cumulativity, Universes} }
Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Jiaxiang Liu, Jean-Pierre Jouannaud, and Mizuhito Ogawa. Confluence of Layered Rewrite Systems. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 423-440, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{liu_et_al:LIPIcs.CSL.2015.423, author = {Liu, Jiaxiang and Jouannaud, Jean-Pierre and Ogawa, Mizuhito}, title = {{Confluence of Layered Rewrite Systems}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {423--440}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.423}, URN = {urn:nbn:de:0030-drops-54293}, doi = {10.4230/LIPIcs.CSL.2015.423}, annote = {Keywords: Layers, confluence, decreasing diagrams, critical pairs, cyclic unification} }