Constructing quotient inductive-inductive types A Kaposi, A Kovács, T Altenkirch Proceedings of the ACM on Programming Languages 3 (POPL), 1-24, 2019 | 72 | 2019 |
Signatures and induction principles for higher inductive-inductive types A Kaposi, A Kovács Logical Methods in Computer Science 16, 2020 | 31 | 2020 |
A syntax for higher inductive-inductive types A Kaposi, A Kovács 3rd International Conference on Formal Structures for Computation and …, 2018 | 31 | 2018 |
Staged compilation with two-level type theory A Kovács Proceedings of the ACM on Programming Languages 6 (ICFP), 540-569, 2022 | 22 | 2022 |
Shallow embedding of type theory is morally correct A Kaposi, A Kovács, N Kraus International Conference on Mathematics of Program Construction, 329-365, 2019 | 16 | 2019 |
Large and infinitary quotient inductive-inductive types A Kovács, A Kaposi Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer …, 2020 | 11 | 2020 |
Generalized universe hierarchies and first-class universe levels A Kovács arXiv preprint arXiv:2103.00223, 2021 | 10 | 2021 |
For finitary induction-induction, induction is enough A Kaposi, A Kovács, A Lafont TYPES 2019: 25th International Conference on Types for Proofs and Programs …, 2019 | 10 | 2019 |
Elaboration with first-class implicit function types A Kovács Proceedings of the ACM on Programming Languages 4 (ICFP), 1-29, 2020 | 4 | 2020 |
Reducing Inductive-Inductive Types to Indexed Inductive Types T Altenkirch, A Kaposi, A Kovács, J Raumer TYPES 2018, 2018 | 3 | 2018 |
Closure-free functional programming in a two-level type theory A Kovács Proceedings of the ACM on Programming Languages 8 (ICFP), 659-692, 2024 | 1 | 2024 |
Closure Conversion for Dependent Type Theory, With Type-Passing Polymorphism A Kovács International Workshop on Types for Proofs and Programs (TYPES), 2018 | 1 | 2018 |
Codes for quotient inductive inductive types A Kaposi, A Kovacs | 1 | 2017 |
Constructing inductive-inductive types using a domain-specific type theory T Altenkirch, P Diviánszky, A Kaposi, A Kovács TYPES 2018, 2018 | | 2018 |
Normalisation by Evaluation for a Type Theory with Large Elimination T Altenkirch, A Kaposi, A Kovács TYPES 2017, 2017 | | 2017 |
Derivation of elimination principles from a context A Kaposi, A Kovács, B Kőműves, P Diviánszky TYPES 2017, 2017 | | 2017 |
Generalizations of Quotient Inductive-Inductive Types A Kovács, A Kaposi EUTYPES-TYPES 2020-Abstracts 4 (1), 2, 0 | | |