Jason Z. S. Hu

18 papers B 2Journal 15Unranked 1
YearRankTypeTitle / Venue / Authors
2025 J jnl
A Dependent Type Theory for Meta-programming with Intensional Analysis.
Proc. ACM Program. Lang.
Jason Z. S. Hu, Brigitte Pientka
2025 J jnl
McTT: A Verified Kernel for a Proof Assistant.
Proc. ACM Program. Lang.
Junyoung Jang, Antoine Gaulin, Jason Z. S. Hu, Brigitte Pientka
2025 J jnl
Normalization by Evaluation for Non-cumulativity.
Proc. ACM Program. Lang.
Shengyi Jiang, Jason Z. S. Hu, Bruno C. d. S. Oliveira
2025 J jnl
The Agda standard library: version 2.0.
J. Open Source Softw.
Matthew L. Daggitt, Guillaume Allais, James McKinna, Andreas Abel, Van Doorn, Nathan, James Wood, Ulf Norell, Donnacha Oisín Kidney, Sergei Meshveliani, Sandro Stucki, Jacques Carette, Alex Rice, Jason Z. S. Hu, Li-yao Xia, Shu-Hung You, Reed Mullanix, Wen Kokke
2024 J jnl
A Layered Approach to Intensional Analysis in Type Theory.
ACM Trans. Program. Lang. Syst.
Jason Z. S. Hu, Brigitte Pientka
2024 J jnl
DeLaM: A Dependent Layered Modal Type Theory for Meta-programming.
CoRR
Jason Z. S. Hu, Brigitte Pientka
2024 — conf
Layered Modal Type Theory - Where Meta-programming Meets Intensional Analysis.
ESOP (1)
Jason Z. S. Hu, Brigitte Pientka
2023 J jnl
Layered Modal Type Theories.
CoRR
Jason Z. S. Hu, Brigitte Pientka
2023 J jnl
Normalization by evaluation for modal dependent type theory.
J. Funct. Program.
Jason Z. S. Hu, Junyoung Jang, Brigitte Pientka
2022 B conf
A Categorical Normalization Proof for the Modal Lambda-Calculus.
MFPS
Jason Z. S. Hu, Brigitte Pientka
2022 J jnl
A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types.
ACM Trans. Comput. Log.
Jason Z. S. Hu, Brigitte Pientka, Ulrich Schöpp
2022 J jnl
A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types.
CoRR
Jason Z. S. Hu, Brigitte Pientka, Ulrich Schöpp
2022 J jnl
An Investigation of Kripke-style Modal Type Theories.
CoRR
Jason Z. S. Hu, Brigitte Pientka
2021 B conf
Formalizing category theory in Agda.
CPP
Jason Z. S. Hu, Jacques Carette
2021 J jnl
Internal Category with Families in Presheaves.
CoRR
Jason Z. S. Hu
2020 J jnl
Proof-relevant Category Theory in Agda.
CoRR
Jason Z. S. Hu, Jacques Carette
2020 J jnl
Undecidability of
Proc. ACM Program. Lang.
Jason Z. S. Hu, Ondrej Lhoták
2019 J jnl
Undecidability of $D_{<: }$ and Its Decidable Fragments.
CoRR
Jason Z. S. Hu, Ondrej Lhoták