Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, and Adam Chlipala. Accelerating Verified-Compiler Development with a Verified Rewriting Engine. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{gross_et_al:LIPIcs.ITP.2022.17, author = {Gross, Jason and Erbsen, Andres and Philipoom, Jade and Poddar-Agrawal, Miraya and Chlipala, Adam}, title = {{Accelerating Verified-Compiler Development with a Verified Rewriting Engine}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {17:1--17:18}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.17}, URN = {urn:nbn:de:0030-drops-167262}, doi = {10.4230/LIPIcs.ITP.2022.17}, annote = {Keywords: compiler verification, rewriting engines, cryptography} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, and Adam Chlipala. Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{gross_et_al:LIPIcs.ITP.2022.18, author = {Gross, Jason and Zimmermann, Th\'{e}o and Poddar-Agrawal, Miraya and Chlipala, Adam}, title = {{Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {18:1--18:18}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.18}, URN = {urn:nbn:de:0030-drops-167273}, doi = {10.4230/LIPIcs.ITP.2022.18}, annote = {Keywords: debugging, automatic test-case reduction, Coq, bug minimizer} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Ornaments for Proof Reuse in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 26:1-26:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{ringer_et_al:LIPIcs.ITP.2019.26, author = {Ringer, Talia and Yazdani, Nathaniel and Leo, John and Grossman, Dan}, title = {{Ornaments for Proof Reuse in Coq}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {26:1--26:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.26}, URN = {urn:nbn:de:0030-drops-110816}, doi = {10.4230/LIPIcs.ITP.2019.26}, annote = {Keywords: ornaments, proof reuse, proof automation} }
Published in: LIPIcs, Volume 71, 2nd Summit on Advances in Programming Languages (SNAPL 2017)
Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, and Katherine Ye. The End of History? Using a Proof Assistant to Replace Language Design with Library Design. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 3:1-3:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{chlipala_et_al:LIPIcs.SNAPL.2017.3, author = {Chlipala, Adam and Delaware, Benjamin and Duchovni, Samuel and Gross, Jason and Pit-Claudel, Cl\'{e}ment and Suriyakarn, Sorawit and Wang, Peng and Ye, Katherine}, title = {{The End of History? Using a Proof Assistant to Replace Language Design with Library Design}}, booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)}, pages = {3:1--3:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-032-3}, ISSN = {1868-8969}, year = {2017}, volume = {71}, editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2017.3}, URN = {urn:nbn:de:0030-drops-71233}, doi = {10.4230/LIPIcs.SNAPL.2017.3}, annote = {Keywords: Domain-specific languages, synthesis, verification, proof assistants, software development} }
Feedback for Dagstuhl Publishing