Nicolai Kraus

Chuangjie Xu

Theor. Comput. Sci., May, 2023

Two-level type theory and applications.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2023

Set-Theoretic and Type-Theoretic Ordinals Coincide.

[BibT_eX]

[DOI]

Tom de Jong

Chuangjie Xu

LICS, 2023

2022

A rewriting coherence theorem with applications in homotopy type theory.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., August, 2022

2021

Connecting Constructive Notions of Ordinals in Homotopy Type Theory.

[BibT_eX]

[DOI]

Chuangjie Xu

Proceedings of the 46th International Symposium on Mathematical Foundations of Computer Science, 2021

Internal ∞-Categorical Models of Dependent Type Theory : Towards 2LTT Eating HoTT.

[BibT_eX]

[DOI]

Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021

2020

Coherence via Wellfoundedness.

[BibT_eX]

[DOI]

CoRR, 2020

Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory.

[BibT_eX]

[DOI]

Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

Control of KNX devices over IEEE 11073 service-oriented device connectivity.

[BibT_eX]

[DOI]

Marc Viertel

Oliver Burgert

Proceedings of the IEEE Conference on Industrial Cyberphysical Systems, 2020

2019

From Cubes to Twisted Cubes via Graph Morphisms in Type Theory.

[BibT_eX]

[DOI]

Gun Pinyo

Proceedings of the 25th International Conference on Types for Proofs and Programs, 2019

Shallow Embedding of Type Theory is Morally Correct.

[BibT_eX]

[DOI]

Ambrus Kaposi

András Kovács

Proceedings of the Mathematics of Program Construction - 13th International Conference, 2019

Path Spaces of Higher Inductive Types in Homotopy Type Theory.

[BibT_eX]

[DOI]

Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, 2019

2018

Univalent higher categories via complete Semi-Segal types.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2018

Free Higher Groups in Homotopy Type Theory.

[BibT_eX]

[DOI]

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Quotient Inductive-Inductive Types.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2018

2017

Space-Valued Diagrams, Type-Theoretically (Extended Abstract).

[BibT_eX]

[DOI]

Christian Sattler

CoRR, 2017

Notions of Anonymous Existence in Martin-Löf Type Theory.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2017

Two-Level Type Theory and Applications.

[BibT_eX]

[DOI]

Danil Annenkov

CoRR, 2017

Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type.

[BibT_eX]

[DOI]

Nils Anders Danielsson

Proceedings of the Foundations of Software Science and Computation Structures, 2017

2016

Constructions with Non-Recursive Higher Inductive Types.

[BibT_eX]

[DOI]

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Extending Homotopy Type Theory with Strict Equality.

[BibT_eX]

[DOI]

Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016

2015

Truncation levels in homotopy type theory.

[BibT_eX]

[DOI]

PhD thesis, 2015

Higher Homotopies in a Hierarchy of Univalent Universes.

[BibT_eX]

[DOI]

Christian Sattler

ACM Trans. Comput. Log., 2015

Functions out of Higher Truncations.

[BibT_eX]

[DOI]

Andrea Vezzosi

Proceedings of the 24th EACSL Annual Conference on Computer Science Logic, 2015

2014

The General Universal Property of the Propositional Truncation.

[BibT_eX]

[DOI]

Proceedings of the 20th International Conference on Types for Proofs and Programs, 2014

2013

On the Hierarchy of Univalent Universes: U(n) is not n-Truncated.

[BibT_eX]

[DOI]

Christian Sattler

CoRR, 2013

Generalizations of Hedberg's Theorem.

[BibT_eX]

[DOI]

Martín Hötzel Escardó

Thierry Coquand

Proceedings of the Typed Lambda Calculi and Applications, 11th International Conference, 2013

2011

A Lambda Term Representation Inspired by Linear Ordered Logic

[BibT_eX]

[DOI]

Andreas Abel