| Constructing quotient inductive-inductive types A Kaposi, A Kovács, T Altenkirch Proceedings of the ACM on Programming Languages 3 (POPL), 1-24, 2019 | 69 | 2019 |
| A syntax for higher inductive-inductive types A Kaposi, A Kovács 3rd International Conference on Formal Structures for Computation and …, 2018 | 30 | 2018 |
| Signatures and induction principles for higher inductive-inductive types A Kaposi, A Kovács Logical Methods in Computer Science 16, 2020 | 29 | 2020 |
| Staged compilation with two-level type theory A Kovács Proceedings of the ACM on Programming Languages 6 (ICFP), 540-569, 2022 | 13 | 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 | 12 | 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 | 10 | 2020 |
| Generalized universe hierarchies and first-class universe levels A Kovács arXiv preprint arXiv:2103.00223, 2021 | 8 | 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 | 7 | 2019 |
| Elaboration with first-class implicit function types A Kovács Proceedings of the ACM on Programming Languages 4 (ICFP), 1-29, 2020 | 3 | 2020 |
| Reducing Inductive-Inductive Types to Indexed Inductive Types T Altenkirch, A Kaposi, A Kovács, J Raumer TYPES 2018, 2018 | 3 | 2018 |
| 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 | | |
Ambrus KaposiEötvös Loránd University, BudapestVerified email at inf.elte.hu
