Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Arve Gengelbach and Johannes Åman Pohjola. A Verified Cyclicity Checker: For Theories with Overloaded Constants. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{gengelbach_et_al:LIPIcs.ITP.2022.15, author = {Gengelbach, Arve and \r{A}man Pohjola, Johannes}, title = {{A Verified Cyclicity Checker: For Theories with Overloaded Constants}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {15:1--15: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.15}, URN = {urn:nbn:de:0030-drops-167240}, doi = {10.4230/LIPIcs.ITP.2022.15}, annote = {Keywords: cyclicity, non-termination, ad-hoc overloading, definitions, Isabelle/HOL} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, and Michael Norrish. Kalas: A Verified, End-To-End Compiler for a Choreographic Language. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{pohjola_et_al:LIPIcs.ITP.2022.27, author = {Pohjola, Johannes \r{A}man and G\'{o}mez-Londo\~{n}o, Alejandro and Shaker, James and Norrish, Michael}, title = {{Kalas: A Verified, End-To-End Compiler for a Choreographic Language}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {27:1--27: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.27}, URN = {urn:nbn:de:0030-drops-167368}, doi = {10.4230/LIPIcs.ITP.2022.27}, annote = {Keywords: Choreographies, Interactive Theorem Proving, Compiler Verification} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Johannes Åman Pohjola, Henrik Rostedt, and Magnus O. Myreen. Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{amanpohjola_et_al:LIPIcs.ITP.2019.32, author = {\r{A}man Pohjola, Johannes and Rostedt, Henrik and Myreen, Magnus O.}, title = {{Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {32:1--32: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.32}, URN = {urn:nbn:de:0030-drops-110872}, doi = {10.4230/LIPIcs.ITP.2019.32}, annote = {Keywords: Program verification, non-termination, liveness, Hoare logic} }
Feedback for Dagstuhl Publishing