Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Max Zeuner and Matthias Hutzler. The Functor of Points Approach to Schemes in Cubical Agda. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 38:1-38:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{zeuner_et_al:LIPIcs.ITP.2024.38, author = {Zeuner, Max and Hutzler, Matthias}, title = {{The Functor of Points Approach to Schemes in Cubical Agda}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {38:1--38: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.38}, URN = {urn:nbn:de:0030-drops-207667}, doi = {10.4230/LIPIcs.ITP.2024.38}, annote = {Keywords: Schemes, Algebraic Geometry, Category Theory, Cubical Agda, Homotopy Type Theory and Univalent Foundations, Constructive Mathematics} }
Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)
Liron Cohen, Bruno da Rocha Paiva, Vincent Rahli, and Ayberk Tosun. Inductive Continuity via Brouwer Trees. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 37:1-37:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{cohen_et_al:LIPIcs.MFCS.2023.37, author = {Cohen, Liron and da Rocha Paiva, Bruno and Rahli, Vincent and Tosun, Ayberk}, title = {{Inductive Continuity via Brouwer Trees}}, booktitle = {48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)}, pages = {37:1--37:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-292-1}, ISSN = {1868-8969}, year = {2023}, volume = {272}, editor = {Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.37}, URN = {urn:nbn:de:0030-drops-185718}, doi = {10.4230/LIPIcs.MFCS.2023.37}, annote = {Keywords: Continuity, Dialogue trees, Stateful computations, Intuitionistic Logic, Extensional Type Theory, Constructive Type Theory, Realizability, Theorem proving, Agda} }
Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó. Type Theory with Explicit Universe Polymorphism. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{bezem_et_al:LIPIcs.TYPES.2022.13, author = {Bezem, Marc and Coquand, Thierry and Dybjer, Peter and Escard\'{o}, Mart{\'\i}n}, title = {{Type Theory with Explicit Universe Polymorphism}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {13:1--13:16}, 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.13}, URN = {urn:nbn:de:0030-drops-184564}, doi = {10.4230/LIPIcs.TYPES.2022.13}, annote = {Keywords: type theory, universes in type theory, universe polymorphism, level-indexed products, constraint-indexed products} }
Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
Max Zeuner and Anders Mörtberg. A Univalent Formalization of Constructive Affine Schemes. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 14:1-14:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{zeuner_et_al:LIPIcs.TYPES.2022.14, author = {Zeuner, Max and M\"{o}rtberg, Anders}, title = {{A Univalent Formalization of Constructive Affine Schemes}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {14:1--14:24}, 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.14}, URN = {urn:nbn:de:0030-drops-184574}, doi = {10.4230/LIPIcs.TYPES.2022.14}, annote = {Keywords: Affine Schemes, Homotopy Type Theory and Univalent Foundations, Cubical Agda, Constructive Mathematics} }
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 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)
Martin Baillon, Assia Mahboubi, and Pierre-Marie Pédrot. Gardening with the Pythia A Model of Continuity in a Dependent Setting. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{baillon_et_al:LIPIcs.CSL.2022.5, author = {Baillon, Martin and Mahboubi, Assia and P\'{e}drot, Pierre-Marie}, title = {{Gardening with the Pythia A Model of Continuity in a Dependent Setting}}, booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)}, pages = {5:1--5:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-218-1}, ISSN = {1868-8969}, year = {2022}, volume = {216}, editor = {Manea, Florin and Simpson, Alex}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.5}, URN = {urn:nbn:de:0030-drops-157256}, doi = {10.4230/LIPIcs.CSL.2022.5}, annote = {Keywords: Type theory, continuity, syntactic model} }
Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)
Liang-Ting Chen and Hsiang-Shang Ko. Realising Intensional S4 and GL Modalities. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{chen_et_al:LIPIcs.CSL.2022.14, author = {Chen, Liang-Ting and Ko, Hsiang-Shang}, title = {{Realising Intensional S4 and GL Modalities}}, booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)}, pages = {14:1--14:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-218-1}, ISSN = {1868-8969}, year = {2022}, volume = {216}, editor = {Manea, Florin and Simpson, Alex}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.14}, URN = {urn:nbn:de:0030-drops-157341}, doi = {10.4230/LIPIcs.CSL.2022.14}, annote = {Keywords: provability, guarded recursion, realisability, modal types, metaprogramming} }
Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
Tom de Jong and Martín Hötzel Escardó. Predicative Aspects of Order Theory in Univalent Foundations. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{dejong_et_al:LIPIcs.FSCD.2021.8, author = {de Jong, Tom and Escard\'{o}, Mart{\'\i}n H\"{o}tzel}, title = {{Predicative Aspects of Order Theory in Univalent Foundations}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {8:1--8:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.8}, URN = {urn:nbn:de:0030-drops-142461}, doi = {10.4230/LIPIcs.FSCD.2021.8}, annote = {Keywords: order theory, constructivity, predicativity, univalent foundations} }
Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
Tom de Jong and Martín Hötzel Escardó. Domain Theory in Constructive and Predicative Univalent Foundations. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{dejong_et_al:LIPIcs.CSL.2021.28, author = {de Jong, Tom and Escard\'{o}, Mart{\'\i}n H\"{o}tzel}, title = {{Domain Theory in Constructive and Predicative Univalent Foundations}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {28:1--28:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.28}, URN = {urn:nbn:de:0030-drops-134625}, doi = {10.4230/LIPIcs.CSL.2021.28}, annote = {Keywords: domain theory, constructivity, predicativity, univalent foundations} }
Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Chuangjie Xu. A Gentzen-Style Monadic Translation of Gödel’s System T. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 25:1-25:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{xu:LIPIcs.FSCD.2020.25, author = {Xu, Chuangjie}, title = {{A Gentzen-Style Monadic Translation of G\"{o}del’s System T}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {25:1--25:17}, 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.25}, URN = {urn:nbn:de:0030-drops-123472}, doi = {10.4230/LIPIcs.FSCD.2020.25}, annote = {Keywords: monadic translation, G\"{o}del’s System T, logical relation, negative translation, majorizability, continuity, bar recursion, Agda} }
Published in: Dagstuhl Reports, Volume 8, Issue 8 (2019)
Andrej Bauer, Martín Escardó, Peter L. Lumsdaine, and Assia Mahboubi. Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341). In Dagstuhl Reports, Volume 8, Issue 8, pp. 130-145, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@Article{bauer_et_al:DagRep.8.8.130, author = {Bauer, Andrej and Escard\'{o}, Mart{\'\i}n and Lumsdaine, Peter L. and Mahboubi, Assia}, title = {{Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341)}}, pages = {130--145}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2019}, volume = {8}, number = {8}, editor = {Bauer, Andrej and Escard\'{o}, Mart{\'\i}n and Lumsdaine, Peter L. and Mahboubi, Assia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.8.8.130}, URN = {urn:nbn:de:0030-drops-102370}, doi = {10.4230/DagRep.8.8.130}, annote = {Keywords: formal methods, formalized mathematics, proof assistant, type theory} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
Auke B. Booij, Martín H. Escardó, Peter LeFanu Lumsdaine, and Michael Shulman. Parametricity, Automorphisms of the Universe, and Excluded Middle. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 7:1-7:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{booij_et_al:LIPIcs.TYPES.2016.7, author = {Booij, Auke B. and Escard\'{o}, Mart{\'\i}n H. and Lumsdaine, Peter LeFanu and Shulman, Michael}, title = {{Parametricity, Automorphisms of the Universe, and Excluded Middle}}, booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)}, pages = {7:1--7:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-065-1}, ISSN = {1868-8969}, year = {2018}, volume = {97}, editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.7}, URN = {urn:nbn:de:0030-drops-98554}, doi = {10.4230/LIPIcs.TYPES.2016.7}, annote = {Keywords: relational parametricity, dependent type theory, univalent foundations, homotopy type theory, excluded middle, classical mathematics, constructive mat} }
Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Martín H. Escardó and Cory M. Knapp. Partial Elements and Recursion via Dominances in Univalent Type Theory. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{escardo_et_al:LIPIcs.CSL.2017.21, author = {Escard\'{o}, Mart{\'\i}n H. and Knapp, Cory M.}, title = {{Partial Elements and Recursion via Dominances in Univalent Type Theory}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {21:1--21:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.21}, URN = {urn:nbn:de:0030-drops-76822}, doi = {10.4230/LIPIcs.CSL.2017.21}, annote = {Keywords: univalent type theory, homotopy type theory, partial function, dominance, recursion theory, computability theory} }
Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
Martín Hötzel Escardó and Chuangjie Xu. The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 153-164, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{hotzelescardo_et_al:LIPIcs.TLCA.2015.153, author = {H\"{o}tzel Escard\'{o}, Mart{\'\i}n and Xu, Chuangjie}, title = {{The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {153--164}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.153}, URN = {urn:nbn:de:0030-drops-51618}, doi = {10.4230/LIPIcs.TLCA.2015.153}, annote = {Keywords: Dependent type, intensional Martin-L\"{o}f type theory, Curry-Howard interpretation, constructive mathematics, Brouwerian continuity axioms, anonymous exi} }
Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)
Martin Escardo, Paulo Oliva, and Thomas Powell. System T and the Product of Selection Functions. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 233-247, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
@InProceedings{escardo_et_al:LIPIcs.CSL.2011.233, author = {Escardo, Martin and Oliva, Paulo and Powell, Thomas}, title = {{System T and the Product of Selection Functions}}, booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL}, pages = {233--247}, 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.233}, URN = {urn:nbn:de:0030-drops-32341}, doi = {10.4230/LIPIcs.CSL.2011.233}, annote = {Keywords: primitive recursion, product of selection functions, finite choice, dialectica interpretation} }
Feedback for Dagstuhl Publishing