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)
James R. Wilcox, Ilya Sergey, and Zachary Tatlock. Programming Language Abstractions for Modularly Verified Distributed Systems. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 19:1-19:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{wilcox_et_al:LIPIcs.SNAPL.2017.19, author = {Wilcox, James R. and Sergey, Ilya and Tatlock, Zachary}, title = {{Programming Language Abstractions for Modularly Verified Distributed Systems}}, booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)}, pages = {19:1--19:12}, 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.19}, URN = {urn:nbn:de:0030-drops-71266}, doi = {10.4230/LIPIcs.SNAPL.2017.19}, annote = {Keywords: Distributed systems, program verification, distributed protocols, domain-specific languages, type systems, dependent types, program logics.} }
Feedback for Dagstuhl Publishing