Παρακολούθηση
András Kovács
András Kovács
Η διεύθυνση ηλεκτρονικού ταχυδρομείου έχει επαληθευτεί στον τομέα inf.elte.hu
Τίτλος
Παρατίθεται από
Παρατίθεται από
Έτος
Constructing quotient inductive-inductive types
A Kaposi, A Kovács, T Altenkirch
Proceedings of the ACM on Programming Languages 3 (POPL), 1-24, 2019
702019
Signatures and induction principles for higher inductive-inductive types
A Kaposi, A Kovács
Logical Methods in Computer Science 16, 2020
322020
A syntax for higher inductive-inductive types
A Kaposi, A Kovács
3rd International Conference on Formal Structures for Computation and …, 2018
302018
Staged compilation with two-level type theory
A Kovács
Proceedings of the ACM on Programming Languages 6 (ICFP), 540-569, 2022
142022
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
132019
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
102020
Generalized universe hierarchies and first-class universe levels
A Kovács
arXiv preprint arXiv:2103.00223, 2021
82021
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
72019
Elaboration with first-class implicit function types
A Kovács
Proceedings of the ACM on Programming Languages 4 (ICFP), 1-29, 2020
32020
Reducing Inductive-Inductive Types to Indexed Inductive Types
T Altenkirch, A Kaposi, A Kovács, J Raumer
TYPES 2018, 2018
32018
Closure Conversion for Dependent Type Theory, With Type-Passing Polymorphism
A Kovács
International Workshop on Types for Proofs and Programs (TYPES), 2018
12018
Codes for quotient inductive inductive types
A Kaposi, A Kovacs
12017
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
Δεν είναι δυνατή η εκτέλεση της ενέργειας από το σύστημα αυτή τη στιγμή. Προσπαθήστε ξανά αργότερα.
Άρθρα 1–16