Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, and Xiaodi Wu. Qafny: A Quantum-Program Verifier. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 24:1-24:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{li_et_al:LIPIcs.ECOOP.2024.24, author = {Li, Liyi and Zhu, Mingwei and Cleaveland, Rance and Nicolellis, Alexander and Lee, Yi and Chang, Le and Wu, Xiaodi}, title = {{Qafny: A Quantum-Program Verifier}}, booktitle = {38th European Conference on Object-Oriented Programming (ECOOP 2024)}, pages = {24:1--24:31}, 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.24}, URN = {urn:nbn:de:0030-drops-208735}, doi = {10.4230/LIPIcs.ECOOP.2024.24}, annote = {Keywords: Quantum Computing, Automated Verification, Separation Logic} }
Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Petar Maksimović, and Philippa Gardner. Matching Plans for Frame Inference in Compositional Reasoning. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{loow_et_al:LIPIcs.ECOOP.2024.26, author = {L\"{o}\"{o}w, Andreas and Nantes-Sobrinho, Daniele and Ayoun, Sacha-\'{E}lie and Maksimovi\'{c}, Petar and Gardner, Philippa}, title = {{Matching Plans for Frame Inference in Compositional Reasoning}}, booktitle = {38th European Conference on Object-Oriented Programming (ECOOP 2024)}, pages = {26:1--26:20}, 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.26}, URN = {urn:nbn:de:0030-drops-208751}, doi = {10.4230/LIPIcs.ECOOP.2024.26}, annote = {Keywords: Compositional reasoning, separation logic, frame inference} }
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 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)
Greta Coraglia and Jacopo Emmenegger. Categorical Models of Subtyping. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 3:1-3:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{coraglia_et_al:LIPIcs.TYPES.2023.3, author = {Coraglia, Greta and Emmenegger, Jacopo}, title = {{Categorical Models of Subtyping}}, booktitle = {29th International Conference on Types for Proofs and Programs (TYPES 2023)}, pages = {3:1--3:19}, 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.3}, URN = {urn:nbn:de:0030-drops-204811}, doi = {10.4230/LIPIcs.TYPES.2023.3}, annote = {Keywords: dependent types, subtyping, coercive subtyping, categorical semantics, categories with families, monad} }
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} }
Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Gabriel Hondet and Frédéric Blanqui. The New Rewriting Engine of Dedukti (System Description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 35:1-35:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{hondet_et_al:LIPIcs.FSCD.2020.35, author = {Hondet, Gabriel and Blanqui, Fr\'{e}d\'{e}ric}, title = {{The New Rewriting Engine of Dedukti}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {35:1--35:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.35}, URN = {urn:nbn:de:0030-drops-123577}, doi = {10.4230/LIPIcs.FSCD.2020.35}, annote = {Keywords: rewriting, higher-order pattern-matching, decision trees} }
Published in: LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017)
Rodolphe Lepigre. PML2: Integrated Program Verification in ML. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 4:1-4:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{lepigre:LIPIcs.TYPES.2017.4, author = {Lepigre, Rodolphe}, title = {{PML2: Integrated Program Verification in ML}}, booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)}, pages = {4:1--4:27}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-071-2}, ISSN = {1868-8969}, year = {2019}, volume = {104}, editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.4}, URN = {urn:nbn:de:0030-drops-100521}, doi = {10.4230/LIPIcs.TYPES.2017.4}, annote = {Keywords: program verification, classical logic, ML-like language, termination checking, Curry-style quantification, implicit subtyping} }
Feedback for Dagstuhl Publishing