20 citations · 33 across the 3 of their papers we have counts for
4 papers
Staged Compilation with Two-Level Type Theory
András Kovács
The aim of staged compilation is to enable metaprogramming in a way such that we have guarantees about the well-formedness of code output, and we can also mix together object-level…
Large and Infinitary Quotient Inductive-Inductive Types
András Kovács, Ambrus Kaposi
Quotient inductive-inductive types (QIITs) are generalized inductive types which allow sorts to be indexed over previously declared sorts, and allow usage of equality constructors.…
Shallow Embedding of Type Theory is Morally Correct
Ambrus Kaposi, András Kovács, Nicolai Kraus
There are multiple ways to formalise the metatheory of type theory. For some purposes, it is enough to consider specific models of a type theory, but sometimes it is necessary to r…
Signatures and Induction Principles for Higher Inductive-Inductive Types
Ambrus Kaposi, András Kovács
Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts…