Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Laurent Théry. Proof Pearl : Playing with the Tower of Hanoi Formally. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 31:1-31:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{thery:LIPIcs.ITP.2021.31, author = {Th\'{e}ry, Laurent}, title = {{Proof Pearl : Playing with the Tower of Hanoi Formally}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {31:1--31:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-188-7}, ISSN = {1868-8969}, year = {2021}, volume = {193}, editor = {Cohen, Liron and Kaliszyk, Cezary}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.31}, URN = {urn:nbn:de:0030-drops-139267}, doi = {10.4230/LIPIcs.ITP.2021.31}, annote = {Keywords: Mathematical logic, Formal proof, Hanoi Tower} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, and Laurent Théry. Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 13:1-13:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@InProceedings{chen_et_al:LIPIcs.ITP.2019.13, author = {Chen, Ran and Cohen, Cyril and L\'{e}vy, Jean-Jacques and Merz, Stephan and Th\'{e}ry, Laurent}, title = {{Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {13:1--13: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.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.13}, URN = {urn:nbn:de:0030-drops-110683}, doi = {10.4230/LIPIcs.ITP.2019.13}, annote = {Keywords: Mathematical logic, Formal proof, Graph algorithm, Program verification} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Florian Steinberg, Laurent Théry, and Holger Thies. Quantitative Continuity and Computable Analysis in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 28:1-28:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@InProceedings{steinberg_et_al:LIPIcs.ITP.2019.28, author = {Steinberg, Florian and Th\'{e}ry, Laurent and Thies, Holger}, title = {{Quantitative Continuity and Computable Analysis in Coq}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {28:1--28:21}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.28}, URN = {urn:nbn:de:0030-drops-110830}, doi = {10.4230/LIPIcs.ITP.2019.28}, annote = {Keywords: computable analysis, Coq, contionuous functionals, discontinuity, closed choice on the naturals} }
Feedback for Dagstuhl Publishing