Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Marco Maggesi and Cosimo Perini Brogi. A Formal Proof of Modal Completeness for Provability Logic. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 26:1-26:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{maggesi_et_al:LIPIcs.ITP.2021.26, author = {Maggesi, Marco and Perini Brogi, Cosimo}, title = {{A Formal Proof of Modal Completeness for Provability Logic}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {26:1--26:18}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.26}, URN = {urn:nbn:de:0030-drops-139215}, doi = {10.4230/LIPIcs.ITP.2021.26}, annote = {Keywords: Provability Logic, Higher-Order Logic, Mechanized Mathematics, HOL Light Theorem Prover} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Florian Steinberg, Laurent Théry, and Holger Thies. Quantitative Continuity and Computable Analysis in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 28:1-28:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{steinberg_et_al:LIPIcs.ITP.2019.28, author = {Steinberg, Florian and Th\'{e}ry, Laurent and Thies, Holger}, title = {{Quantitative Continuity and Computable Analysis in Coq}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {28:1--28:21}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.28}, URN = {urn:nbn:de:0030-drops-110830}, doi = {10.4230/LIPIcs.ITP.2019.28}, annote = {Keywords: computable analysis, Coq, contionuous functionals, discontinuity, closed choice on the naturals} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Benedikt Ahrens, Dan Frumin, Marco Maggesi, and Niels van der Weide. Bicategories in Univalent Foundations. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 5:1-5:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@InProceedings{ahrens_et_al:LIPIcs.FSCD.2019.5, author = {Ahrens, Benedikt and Frumin, Dan and Maggesi, Marco and van der Weide, Niels}, title = {{Bicategories in Univalent Foundations}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {5:1--5:17}, 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.5}, URN = {urn:nbn:de:0030-drops-105124}, doi = {10.4230/LIPIcs.FSCD.2019.5}, annote = {Keywords: bicategory theory, univalent mathematics, dependent type theory, Coq} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi. Modular Specification of Monads Through Higher-Order Presentations. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 6:1-6:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@InProceedings{ahrens_et_al:LIPIcs.FSCD.2019.6, author = {Ahrens, Benedikt and Hirschowitz, Andr\'{e} and Lafont, Ambroise and Maggesi, Marco}, title = {{Modular Specification of Monads Through Higher-Order Presentations}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {6:1--6:19}, 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.6}, URN = {urn:nbn:de:0030-drops-105136}, doi = {10.4230/LIPIcs.FSCD.2019.6}, annote = {Keywords: free monads, presentation of monads, initial semantics, signatures, syntax, monadic substitution, computer-checked proofs} }
Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi. High-Level Signatures and Initial Semantics. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 4:1-4:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
@InProceedings{ahrens_et_al:LIPIcs.CSL.2018.4, author = {Ahrens, Benedikt and Hirschowitz, Andr\'{e} and Lafont, Ambroise and Maggesi, Marco}, title = {{High-Level Signatures and Initial Semantics}}, booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)}, pages = {4:1--4:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-088-0}, ISSN = {1868-8969}, year = {2018}, volume = {119}, editor = {Ghica, Dan R. and Jung, Achim}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.4}, URN = {urn:nbn:de:0030-drops-96713}, doi = {10.4230/LIPIcs.CSL.2018.4}, annote = {Keywords: initial semantics, signatures, syntax, monadic substitution, computer-checked proofs} }
Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Benedikt Ahrens and Régis Spadotti. Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 1-26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{ahrens_et_al:LIPIcs.TYPES.2014.1, author = {Ahrens, Benedikt and Spadotti, R\'{e}gis}, title = {{Terminal Semantics for Codata Types in Intensional Martin-L\"{o}f Type Theory}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {1--26}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.1}, URN = {urn:nbn:de:0030-drops-54891}, doi = {10.4230/LIPIcs.TYPES.2014.1}, annote = {Keywords: relative comonad, Martin-L\"{o}f type theory, coinductive type, computer theorem proving} }
Feedback for Dagstuhl Publishing