Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Peter Lammich. Generating Verified LLVM from Isabelle/HOL. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{lammich:LIPIcs.ITP.2019.22, author = {Lammich, Peter}, title = {{Generating Verified LLVM from Isabelle/HOL}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {22:1--22: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.22}, URN = {urn:nbn:de:0030-drops-110777}, doi = {10.4230/LIPIcs.ITP.2019.22}, annote = {Keywords: Isabelle/HOL, LLVM, Separation Logic, Verification Condition Generator, Code Generation} }
Published in: LIPIcs, Volume 53, 15th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2016)
Boris Aronov, Matias Korman, Simon Pratt, André van Renssen, and Marcel Roeloffzen. Time-Space Trade-offs for Triangulating a Simple Polygon. In 15th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 53, pp. 30:1-30:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{aronov_et_al:LIPIcs.SWAT.2016.30, author = {Aronov, Boris and Korman, Matias and Pratt, Simon and van Renssen, André and Roeloffzen, Marcel}, title = {{Time-Space Trade-offs for Triangulating a Simple Polygon}}, booktitle = {15th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2016)}, pages = {30:1--30:12}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-011-8}, ISSN = {1868-8969}, year = {2016}, volume = {53}, editor = {Pagh, Rasmus}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SWAT.2016.30}, URN = {urn:nbn:de:0030-drops-60522}, doi = {10.4230/LIPIcs.SWAT.2016.30}, annote = {Keywords: simple polygon, triangulation, shortest path, time-space trade-off} }
Published in: LIPIcs, Volume 51, 32nd International Symposium on Computational Geometry (SoCG 2016)
Timothy M. Chan and Simon Pratt. Two Approaches to Building Time-Windowed Geometric Data Structures. In 32nd International Symposium on Computational Geometry (SoCG 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 51, pp. 28:1-28:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{chan_et_al:LIPIcs.SoCG.2016.28, author = {Chan, Timothy M. and Pratt, Simon}, title = {{Two Approaches to Building Time-Windowed Geometric Data Structures}}, booktitle = {32nd International Symposium on Computational Geometry (SoCG 2016)}, pages = {28:1--28:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-009-5}, ISSN = {1868-8969}, year = {2016}, volume = {51}, editor = {Fekete, S\'{a}ndor and Lubiw, Anna}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2016.28}, URN = {urn:nbn:de:0030-drops-59201}, doi = {10.4230/LIPIcs.SoCG.2016.28}, annote = {Keywords: time window, geometric data structures, range searching, dynamic convex hull} }
Feedback for Dagstuhl Publishing