Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Vlastimil Dort, Yufeng Li, Ondřej Lhoták, and Pavel Parízek. Pure Methods for roDOT. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 13:1-13:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{dort_et_al:LIPIcs.ECOOP.2024.13, author = {Dort, Vlastimil and Li, Yufeng and Lhot\'{a}k, Ond\v{r}ej and Par{\'\i}zek, Pavel}, title = {{Pure Methods for roDOT}}, booktitle = {38th European Conference on Object-Oriented Programming (ECOOP 2024)}, pages = {13:1--13:29}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-341-6}, ISSN = {1868-8969}, year = {2024}, volume = {313}, editor = {Aldrich, Jonathan and Salvaneschi, Guido}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.13}, URN = {urn:nbn:de:0030-drops-208624}, doi = {10.4230/LIPIcs.ECOOP.2024.13}, annote = {Keywords: type systems, DOT calculus, pure methods} }
Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Cormac Flanagan and Stephen N. Freund. Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 16:1-16:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{flanagan_et_al:LIPIcs.ECOOP.2024.16, author = {Flanagan, Cormac and Freund, Stephen N.}, title = {{Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning}}, booktitle = {38th European Conference on Object-Oriented Programming (ECOOP 2024)}, pages = {16:1--16:29}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-341-6}, ISSN = {1868-8969}, year = {2024}, volume = {313}, editor = {Aldrich, Jonathan and Salvaneschi, Guido}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.16}, URN = {urn:nbn:de:0030-drops-208654}, doi = {10.4230/LIPIcs.ECOOP.2024.16}, annote = {Keywords: concurrent program verification, reduction, rely-guarantee reasoning, synchronization} }
Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Nisarg Patel, Dennis Shasha, and Thomas Wies. Verifying Lock-Free Search Structure Templates. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 30:1-30:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{patel_et_al:LIPIcs.ECOOP.2024.30, author = {Patel, Nisarg and Shasha, Dennis and Wies, Thomas}, title = {{Verifying Lock-Free Search Structure Templates}}, booktitle = {38th European Conference on Object-Oriented Programming (ECOOP 2024)}, pages = {30:1--30:28}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-341-6}, ISSN = {1868-8969}, year = {2024}, volume = {313}, editor = {Aldrich, Jonathan and Salvaneschi, Guido}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.30}, URN = {urn:nbn:de:0030-drops-208797}, doi = {10.4230/LIPIcs.ECOOP.2024.30}, annote = {Keywords: skiplists, lock-free, separation logic, linearizability, future-dependent linearization points, hindsight reasoning} }
Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Bas van den Heuvel, Farzaneh Derakhshan, and Stephanie Balzer. Information Flow Control in Cyclic Process Networks. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 40:1-40:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{vandenheuvel_et_al:LIPIcs.ECOOP.2024.40, author = {van den Heuvel, Bas and Derakhshan, Farzaneh and Balzer, Stephanie}, title = {{Information Flow Control in Cyclic Process Networks}}, booktitle = {38th European Conference on Object-Oriented Programming (ECOOP 2024)}, pages = {40:1--40:30}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-341-6}, ISSN = {1868-8969}, year = {2024}, volume = {313}, editor = {Aldrich, Jonathan and Salvaneschi, Guido}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.40}, URN = {urn:nbn:de:0030-drops-208891}, doi = {10.4230/LIPIcs.ECOOP.2024.40}, annote = {Keywords: Cyclic process networks, linear session types, logical relations, deadlock-sensitive noninterference} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Marc Hermes and Robbert Krebbers. Modular Verification of Intrusive List and Tree Data Structures in Separation Logic. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{hermes_et_al:LIPIcs.ITP.2024.19, author = {Hermes, Marc and Krebbers, Robbert}, title = {{Modular Verification of Intrusive List and Tree Data Structures in Separation Logic}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {19:1--19:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.19}, URN = {urn:nbn:de:0030-drops-207478}, doi = {10.4230/LIPIcs.ITP.2024.19}, annote = {Keywords: Separation Logic, Program Verification, Data Structures, Iris, Coq} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Vincent Jackson, Toby Murray, and Christine Rizkallah. A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{jackson_et_al:LIPIcs.ITP.2024.23, author = {Jackson, Vincent and Murray, Toby and Rizkallah, Christine}, title = {{A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {23:1--23:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.23}, URN = {urn:nbn:de:0030-drops-207510}, doi = {10.4230/LIPIcs.ITP.2024.23}, annote = {Keywords: verification, concurrency, rely-guarantee, separation logic, resource algebras} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Audrey Seo, Christopher Lam, Dan Grossman, and Talia Ringer. Correctly Compiling Proofs About Programs Without Proving Compilers Correct. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{seo_et_al:LIPIcs.ITP.2024.33, author = {Seo, Audrey and Lam, Christopher and Grossman, Dan and Ringer, Talia}, title = {{Correctly Compiling Proofs About Programs Without Proving Compilers Correct}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {33:1--33:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.33}, URN = {urn:nbn:de:0030-drops-207612}, doi = {10.4230/LIPIcs.ITP.2024.33}, annote = {Keywords: proof transformations, compiler validation, program logics, proof engineering} }
Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)
Mrudula Balachander, Emmanuel Filiot, and Raffaella Gentilini. Passive Learning of Regular Data Languages in Polynomial Time and Data. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{balachander_et_al:LIPIcs.CONCUR.2024.10, author = {Balachander, Mrudula and Filiot, Emmanuel and Gentilini, Raffaella}, title = {{Passive Learning of Regular Data Languages in Polynomial Time and Data}}, booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)}, pages = {10:1--10:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-339-3}, ISSN = {1868-8969}, year = {2024}, volume = {311}, editor = {Majumdar, Rupak and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.10}, URN = {urn:nbn:de:0030-drops-207829}, doi = {10.4230/LIPIcs.CONCUR.2024.10}, annote = {Keywords: Register automata, passive learning, automata over infinite alphabets} }
Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)
Juan C. Jaramillo, Dan Frumin, and Jorge A. Pérez. Around Classical and Intuitionistic Linear Processes. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{jaramillo_et_al:LIPIcs.CONCUR.2024.30, author = {Jaramillo, Juan C. and Frumin, Dan and P\'{e}rez, Jorge A.}, title = {{Around Classical and Intuitionistic Linear Processes}}, booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)}, pages = {30:1--30:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-339-3}, ISSN = {1868-8969}, year = {2024}, volume = {311}, editor = {Majumdar, Rupak and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.30}, URN = {urn:nbn:de:0030-drops-208026}, doi = {10.4230/LIPIcs.CONCUR.2024.30}, annote = {Keywords: Process calculi, session types, linear logic} }
Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)
Stefan Kiefer and Qiyi Tang. Minimising the Probabilistic Bisimilarity Distance. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{kiefer_et_al:LIPIcs.CONCUR.2024.32, author = {Kiefer, Stefan and Tang, Qiyi}, title = {{Minimising the Probabilistic Bisimilarity Distance}}, booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)}, pages = {32:1--32:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-339-3}, ISSN = {1868-8969}, year = {2024}, volume = {311}, editor = {Majumdar, Rupak and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.32}, URN = {urn:nbn:de:0030-drops-208049}, doi = {10.4230/LIPIcs.CONCUR.2024.32}, annote = {Keywords: Markov decision processes, Markov chains} }
Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)
Joris Ceulemans, Andreas Nuyts, and Dominique Devriese. A Sound and Complete Substitution Algorithm for Multimode Type Theory. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{ceulemans_et_al:LIPIcs.TYPES.2023.4, author = {Ceulemans, Joris and Nuyts, Andreas and Devriese, Dominique}, title = {{A Sound and Complete Substitution Algorithm for Multimode Type Theory}}, booktitle = {29th International Conference on Types for Proofs and Programs (TYPES 2023)}, pages = {4:1--4:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-332-4}, ISSN = {1868-8969}, year = {2024}, volume = {303}, editor = {Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.4}, URN = {urn:nbn:de:0030-drops-204826}, doi = {10.4230/LIPIcs.TYPES.2023.4}, annote = {Keywords: dependent type theory, modalities, multimode type theory, explicit substitutions, substitution algorithm} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
G. A. Kavvos. Two-Dimensional Kripke Semantics I: Presheaves. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 14:1-14:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{kavvos:LIPIcs.FSCD.2024.14, author = {Kavvos, G. A.}, title = {{Two-Dimensional Kripke Semantics I: Presheaves}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {14:1--14:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.14}, URN = {urn:nbn:de:0030-drops-203438}, doi = {10.4230/LIPIcs.FSCD.2024.14}, annote = {Keywords: modal logic, categorical semantics, Kripke semantics, duality, open maps} }
Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)
Jonathan Sterling, Daniel Gratzer, and Lars Birkedal. Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 47:1-47:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{sterling_et_al:LIPIcs.CSL.2024.47, author = {Sterling, Jonathan and Gratzer, Daniel and Birkedal, Lars}, title = {{Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {47:1--47:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.47}, URN = {urn:nbn:de:0030-drops-196901}, doi = {10.4230/LIPIcs.CSL.2024.47}, annote = {Keywords: univalent foundations, homotopy type theory, impredicative encodings, synthetic guarded domain theory, guarded recursion, higher-order store, reference types} }
Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
Philipp Stassen, Daniel Gratzer, and Lars Birkedal. {mitten}: A Flexible Multimodal Proof Assistant. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{stassen_et_al:LIPIcs.TYPES.2022.6, author = {Stassen, Philipp and Gratzer, Daniel and Birkedal, Lars}, title = {{\{mitten\}: A Flexible Multimodal Proof Assistant}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {6:1--6:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-285-3}, ISSN = {1868-8969}, year = {2023}, volume = {269}, editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.6}, URN = {urn:nbn:de:0030-drops-184498}, doi = {10.4230/LIPIcs.TYPES.2022.6}, annote = {Keywords: Dependent type theory, guarded recursion, modal type theory, proof assistants} }
Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)
Robbert Krebbers. Interactive and Automated Proofs in Modal Separation Logic (Invited Talk). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{krebbers:LIPIcs.ITP.2023.2, author = {Krebbers, Robbert}, title = {{Interactive and Automated Proofs in Modal Separation Logic}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {2:1--2:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-284-6}, ISSN = {1868-8969}, year = {2023}, volume = {268}, editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.2}, URN = {urn:nbn:de:0030-drops-183770}, doi = {10.4230/LIPIcs.ITP.2023.2}, annote = {Keywords: Program Verification, Separation Logic, Step-Indexing, Modal Logic, Interactive Theorem Proving, Proof Automation, Iris, Coq} }
Feedback for Dagstuhl Publishing