5 papers
DeLaM: A Dependent Layered Modal Type Theory for Meta-programming
Jason Z. S. Hu, Brigitte Pientka
We scale layered modal type theory to dependent types, introducing DeLaM, dependent layered modal type theory. This type theory is novel in that we have one uniform type theory in…
Layered Modal Type Theories
Jason Z. S. Hu, Brigitte Pientka
We introduce layers to modal type theories, which subsequently enables type theories for pattern matching on code in meta-programming and clean and straightforward semantics.
Internal Category with Families in Presheaves
Jason Z. S. Hu
In this note, we review a construction of category with families (CwF) in a presheaf category. When the base category of a presheaf category is a CwF, we internalize this CwF struc…
Formalizing of Category Theory in Agda
Jason Z. S. Hu, Jacques Carette
The generality and pervasiness of category theory in modern mathematics makes it a frequent and useful target of formalization. It is however quite challenging to formalize, for a…
Undecidability of and Its Decidable Fragments
Jason Hu, Ondřej Lhoták
Dependent Object Types (DOT) is a calculus with path dependent types, intersection types, and object self-references, which serves as the core calculus of Scala 3. Although the cal…