Niels van der Weide

Orcid: 0000-0003-1146-4161

According to our database1, Niels van der Weide authored at least 20 papers between 2017 and 2025.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

2017
2018
2019
2020
2021
2022
2023
2024
2025
0
1
2
3
4
5
6
1
1
1
3
1
2
4
1
1
1
3
1

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2025
The Formal Theory of Monads, Univalently.
Log. Methods Comput. Sci., 2025

Insights from Univalent Foundations: A Case Study Using Double Categories.
Proceedings of the 33rd EACSL Annual Conference on Computer Science Logic, 2025

Intrinsically Correct Sorting in Cubical Agda.
Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2025

2024
The internal languages of univalent categories.
CoRR, 2024

Univalent Enriched Categories and the Enriched Rezk Completion.
Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction, 2024

Univalent Double Categories.
Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

Displayed Monoidal Categories for the Semantics of Linear Logic.
Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

The Interval Domain in Homotopy Type Theory.
Proceedings of the Logics and Type Systems in Theory and Practice, 2024

2023
Bicategorical type theory: semantics and syntax.
Math. Struct. Comput. Sci., 2023

Certifying Higher-Order Polynomial Interpretations.
Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

2022
Semantics for two-dimensional type theory.
Proceedings of the LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2, 2022

2021
Bicategories in univalent foundations.
Math. Struct. Comput. Sci., 2021

Constructing Higher Inductive Types as Groupoid Quotients.
Log. Methods Comput. Sci., 2021

Formalizing Higher-Order Termination in Coq.
CoRR, 2021

2020
Constructing Higher Inductive Types as Groupoid Quotients.
Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

2019
The Construction of Set-Truncated Higher Inductive Types.
Proceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics, 2019

Guarded Recursion in Agda via Sized Types.
Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction, 2019

Bicategories in Univalent Foundations.
Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction, 2019

2018
Finite sets in homotopy type theory.
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017
Higher Inductive Types in Programming.
J. Univers. Comput. Sci., 2017


  Loading...