Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)
Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu. Connecting Constructive Notions of Ordinals in Homotopy Type Theory. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 70:1-70:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{kraus_et_al:LIPIcs.MFCS.2021.70, author = {Kraus, Nicolai and Nordvall Forsberg, Fredrik and Xu, Chuangjie}, title = {{Connecting Constructive Notions of Ordinals in Homotopy Type Theory}}, booktitle = {46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)}, pages = {70:1--70:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-201-3}, ISSN = {1868-8969}, year = {2021}, volume = {202}, editor = {Bonchi, Filippo and Puglisi, Simon J.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.70}, URN = {urn:nbn:de:0030-drops-145100}, doi = {10.4230/LIPIcs.MFCS.2021.70}, annote = {Keywords: Constructive ordinals, Cantor normal forms, Brouwer trees} }
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: 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