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 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Magnus O. Myreen. The CakeML Project’s Quest for Ever Stronger Correctness Theorems (Invited Paper). In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 1:1-1:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{myreen:LIPIcs.ITP.2021.1, author = {Myreen, Magnus O.}, title = {{The CakeML Project’s Quest for Ever Stronger Correctness Theorems}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {1:1--1:10}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.1}, URN = {urn:nbn:de:0030-drops-138963}, doi = {10.4230/LIPIcs.ITP.2021.1}, annote = {Keywords: Program verification, interactive theorem proving} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Robert Sison and Toby Murray. Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 27:1-27:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{sison_et_al:LIPIcs.ITP.2019.27, author = {Sison, Robert and Murray, Toby}, title = {{Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {27:1--27: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.27}, URN = {urn:nbn:de:0030-drops-110829}, doi = {10.4230/LIPIcs.ITP.2019.27}, annote = {Keywords: Secure compilation, Information flow security, Concurrency, 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