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 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} }
Feedback for Dagstuhl Publishing