Two-level type theory and applications D Annenkov, P Capriotti, N Kraus, C Sattler Mathematical Structures in Computer Science 33 (8), 688-743, 2023 | 93 | 2023 |
The Frobenius condition, right properness, and uniform fibrations N Gambino, C Sattler Journal of Pure and Applied Algebra 221 (12), 3027-3068, 2017 | 68 | 2017 |
The equivalence extension property and model structures C Sattler arXiv preprint arXiv:1704.06911, 2017 | 42 | 2017 |
Gluing for type theory A Kaposi, S Huber, C Sattler 4th International Conference on Formal Structures for Computation and …, 2019 | 41 | 2019 |
Homotopy canonicity for cubical type theory T Coquand, S Huber, C Sattler 4th International Conference on Formal Structures for Computation and …, 2019 | 30 | 2019 |
Higher homotopies in a hierarchy of univalent universes N Kraus, C Sattler ACM Transactions on Computational Logic (TOCL) 16 (2), 1-12, 2015 | 21 | 2015 |
Constructive sheaf models of type theory T Coquand, F Ruch, C Sattler Mathematical Structures in Computer Science 31 (9), 979-1002, 2021 | 17 | 2021 |
Normalization by evaluation for call-by-push-value and polarized lambda calculus A Abel, C Sattler Proceedings of the 21st International Symposium on Principles and Practice …, 2019 | 17 | 2019 |
The constructive Kan–Quillen model structure: two new proofs N Gambino, C Sattler, K Szumiło The Quarterly Journal of Mathematics 73 (4), 1307-1373, 2022 | 16 | 2022 |
For the metatheory of type theory, internal sconing is enough R Bocquet, A Kaposi, C Sattler arXiv preprint arXiv:2302.05190, 2023 | 13 | 2023 |
On the directed univalence axiom E Riehl, E Cavallo, C Sattler Talk slides, AMS Special Session on Homotopy Type Theory, Joint Mathematics …, 2018 | 13 | 2018 |
Space-valued diagrams, type-theoretically N Kraus, C Sattler arXiv preprint arXiv:1704.04543, 2017 | 12 | 2017 |
Constructing a universe for the setoid model. T Altenkirch, S Boulier, A Kaposi, C Sattler, F Sestini FoSSaCS, 1-21, 2021 | 10 | 2021 |
Cubical models of -categories B Doherty, C Kapulkin, Z Lindsey, C Sattler arXiv preprint arXiv:2005.04853, 2020 | 10 | 2020 |
Uniform fibrations and the Frobenius condition N Gambino, C Sattler arXiv preprint arXiv:1510.00669, 2015 | 10 | 2015 |
Relative induction principles for type theories R Bocquet, A Kaposi, C Sattler arXiv preprint arXiv:2102.11649, 2021 | 9 | 2021 |
Do cubical models of type theory also model homotopy types C Sattler Talk at Workshop on Types, Homotopy Type theory, and Verification at …, 2018 | 9 | 2018 |
Idempotent completion of cubes in posets C Sattler arXiv preprint arXiv:1805.04126, 2018 | 8 | 2018 |
Canonicity and homotopy canonicity for cubical type theory T Coquand, S Huber, C Sattler Logical Methods in Computer Science 18, 2022 | 7 | 2022 |
Two-Level Type Theory and Applications.(2017) D Annenkov, P Capriotti, N Kraus, C Sattler URL: http://arxiv. org/abs/1705.03307, 2017 | 6 | 2017 |