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} }
Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)
Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, and Lars Birkedal. Modular Verification of State-Based CRDTs in Separation Logic. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 22:1-22:27, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{nieto_et_al:LIPIcs.ECOOP.2023.22, author = {Nieto, Abel and Daby-Seesaram, Arnaud and Gondelman, L\'{e}on and Timany, Amin and Birkedal, Lars}, title = {{Modular Verification of State-Based CRDTs in Separation Logic}}, booktitle = {37th European Conference on Object-Oriented Programming (ECOOP 2023)}, pages = {22:1--22:27}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-281-5}, ISSN = {1868-8969}, year = {2023}, volume = {263}, editor = {Ali, Karim 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.2023.22}, URN = {urn:nbn:de:0030-drops-182154}, doi = {10.4230/LIPIcs.ECOOP.2023.22}, annote = {Keywords: separation logic, distributed systems, CRDT, replicated data type, formal verification} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Jonathan Sterling and Robert Harper. Sheaf Semantics of Termination-Insensitive Noninterference. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 5:1-5:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{sterling_et_al:LIPIcs.FSCD.2022.5, author = {Sterling, Jonathan and Harper, Robert}, title = {{Sheaf Semantics of Termination-Insensitive Noninterference}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {5:1--5:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-233-4}, ISSN = {1868-8969}, year = {2022}, volume = {228}, editor = {Felty, Amy P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.5}, URN = {urn:nbn:de:0030-drops-162869}, doi = {10.4230/LIPIcs.FSCD.2022.5}, annote = {Keywords: information flow, noninterference, denotational semantics, phase distinction, Artin gluing, modal type theory, topos theory, synthetic domain theory, synthetic Tait computability} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Daniel Gratzer and Lars Birkedal. A Stratified Approach to Löb Induction. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 23:1-23:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{gratzer_et_al:LIPIcs.FSCD.2022.23, author = {Gratzer, Daniel and Birkedal, Lars}, title = {{A Stratified Approach to L\"{o}b Induction}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {23:1--23:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-233-4}, ISSN = {1868-8969}, year = {2022}, volume = {228}, editor = {Felty, Amy P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.23}, URN = {urn:nbn:de:0030-drops-163048}, doi = {10.4230/LIPIcs.FSCD.2022.23}, annote = {Keywords: Dependent type theory, guarded recursion, modal type theory, canonicity, categorical gluing} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. Cubical Syntax for Reflection-Free Extensional Equality. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 31:1-31:25, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@InProceedings{sterling_et_al:LIPIcs.FSCD.2019.31, author = {Sterling, Jonathan and Angiuli, Carlo and Gratzer, Daniel}, title = {{Cubical Syntax for Reflection-Free Extensional Equality}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {31:1--31:25}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.31}, URN = {urn:nbn:de:0030-drops-105387}, doi = {10.4230/LIPIcs.FSCD.2019.31}, annote = {Keywords: Dependent type theory, extensional equality, cubical type theory, categorical gluing, canonicity} }
Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Valeria Vignudelli. Proof Techniques for Program Equivalence in Probabilistic Higher-Order Languages (Invited Talk). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 4:1-4:2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
@InProceedings{vignudelli:LIPIcs.FSCD.2018.4, author = {Vignudelli, Valeria}, title = {{Proof Techniques for Program Equivalence in Probabilistic Higher-Order Languages}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {4:1--4:2}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.4}, URN = {urn:nbn:de:0030-drops-91749}, doi = {10.4230/LIPIcs.FSCD.2018.4}, annote = {Keywords: Lambda Calculus, Contextual Equivalence, Bisimulation, Probabilistic Programming Languages} }
Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
Lars Birkedal, Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi. Guarded Cubical Type Theory: Path Equality for Guarded Recursion. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 23:1-23:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)
@InProceedings{birkedal_et_al:LIPIcs.CSL.2016.23, author = {Birkedal, Lars and Bizjak, Ale\v{s} and Clouston, Ranald and Grathwohl, Hans Bugge and Spitters, Bas and Vezzosi, Andrea}, title = {{Guarded Cubical Type Theory: Path Equality for Guarded Recursion}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {23:1--23:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.23}, URN = {urn:nbn:de:0030-drops-65638}, doi = {10.4230/LIPIcs.CSL.2016.23}, annote = {Keywords: Guarded Recursion, Dependent Type Theory, Cubical Type Theory, Denotational Semantics, Homotopy Type Theory} }
Published in: Dagstuhl Reports, Volume 5, Issue 5 (2016)
Lars Birkedal, Derek Dreyer, Philippa Gardner, and Zhong Shao. Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191). In Dagstuhl Reports, Volume 5, Issue 5, pp. 1-23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)
@Article{birkedal_et_al:DagRep.5.5.1, author = {Birkedal, Lars and Dreyer, Derek and Gardner, Philippa and Shao, Zhong}, title = {{Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191)}}, pages = {1--23}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2015}, volume = {5}, number = {5}, editor = {Birkedal, Lars and Dreyer, Derek and Gardner, Philippa and Shao, Zhong}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.5.1}, URN = {urn:nbn:de:0030-drops-53565}, doi = {10.4230/DagRep.5.5.1}, annote = {Keywords: Verification of Concurrent Programs (Models, Logics, Automated Analysis), Concurrent Programming} }
Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)
Lars Birkedal, Filip Sieczkowski, and Jacob Thamsborg. A Concurrent Logical Relation. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 107-121, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)
@InProceedings{birkedal_et_al:LIPIcs.CSL.2012.107, author = {Birkedal, Lars and Sieczkowski, Filip and Thamsborg, Jacob}, title = {{A Concurrent Logical Relation}}, booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL}, pages = {107--121}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-42-2}, ISSN = {1868-8969}, year = {2012}, volume = {16}, editor = {C\'{e}gielski, Patrick and Durand, Arnaud}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.107}, URN = {urn:nbn:de:0030-drops-36671}, doi = {10.4230/LIPIcs.CSL.2012.107}, annote = {Keywords: verification, logical relation, concurrency, type and effect system} }
Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)
Jan Schwinghammer and Lars Birkedal. Step-Indexed Relational Reasoning for Countable Nondeterminism. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 512-524, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2011)
@InProceedings{schwinghammer_et_al:LIPIcs.CSL.2011.512, author = {Schwinghammer, Jan and Birkedal, Lars}, title = {{Step-Indexed Relational Reasoning for Countable Nondeterminism}}, booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL}, pages = {512--524}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-32-3}, ISSN = {1868-8969}, year = {2011}, volume = {12}, editor = {Bezem, Marc}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.512}, URN = {urn:nbn:de:0030-drops-32535}, doi = {10.4230/LIPIcs.CSL.2011.512}, annote = {Keywords: countable choice, lambda calculus, program equivalence} }
Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)
Amal Ahmed, Nick Benton, Lars Birkedal, and Martin Hofmann. 10351 Abstracts Collection – Modelling, Controlling and Reasoning About State. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)
@InProceedings{ahmed_et_al:DagSemProc.10351.1, author = {Ahmed, Amal and Benton, Nick and Birkedal, Lars and Hofmann, Martin}, title = {{10351 Abstracts Collection – Modelling, Controlling and Reasoning About State}}, booktitle = {Modelling, Controlling and Reasoning About State}, pages = {1--16}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {10351}, editor = {Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.1}, URN = {urn:nbn:de:0030-drops-28116}, doi = {10.4230/DagSemProc.10351.1}, annote = {Keywords: Mutable State, Program Logics, Semantics, Type Systems, Verification} }
Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)
Amal Ahmed, Nick Benton, Lars Birkedal, and Martin Hofmann. 10351 Executive Summary – Modelling, Controlling and Reasoning About State. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-4, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)
@InProceedings{ahmed_et_al:DagSemProc.10351.2, author = {Ahmed, Amal and Benton, Nick and Birkedal, Lars and Hofmann, Martin}, title = {{10351 Executive Summary – Modelling, Controlling and Reasoning About State}}, booktitle = {Modelling, Controlling and Reasoning About State}, pages = {1--4}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {10351}, editor = {Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.2}, URN = {urn:nbn:de:0030-drops-28108}, doi = {10.4230/DagSemProc.10351.2}, annote = {Keywords: Mutable State, Program Logics, Semantics, Type Systems, Verification} }
Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)
Robert Dockins and Aquinas Hobor. A Theory of Termination via Indirection. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-12, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)
@InProceedings{dockins_et_al:DagSemProc.10351.3, author = {Dockins, Robert and Hobor, Aquinas}, title = {{A Theory of Termination via Indirection}}, booktitle = {Modelling, Controlling and Reasoning About State}, pages = {1--12}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {10351}, editor = {Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.3}, URN = {urn:nbn:de:0030-drops-28050}, doi = {10.4230/DagSemProc.10351.3}, annote = {Keywords: Step-indexed Models, Termination} }
Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)
Vasileios Koutavas, Paul Blain Levy, and Eijiro Sumii. Limitations of Applicative Bisimulation (Preliminary Report). In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-9, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)
@InProceedings{koutavas_et_al:DagSemProc.10351.4, author = {Koutavas, Vasileios and Levy, Paul Blain and Sumii, Eijiro}, title = {{Limitations of Applicative Bisimulation (Preliminary Report)}}, booktitle = {Modelling, Controlling and Reasoning About State}, pages = {1--9}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {10351}, editor = {Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.4}, URN = {urn:nbn:de:0030-drops-28074}, doi = {10.4230/DagSemProc.10351.4}, annote = {Keywords: Imperative languages, higher-order functions, local state} }
Feedback for Dagstuhl Publishing