Jason Z. S. Hu
where else to find them
no profile links on file
what they talk about
where they keep going back
no series more than once — all 3 in the filters
on a stage with
all 4 in the filters
who talks about the same things
- Brigitte Pientka15 talks
- Andreas Abel6 talks
- Nicolas Tabareau14 talks
- Kenji Maillard11 talks
- Amal Ahmed25 talks
- Stephanie Weirich14 talks
| title | conference | date |
|---|---|---|
| Normalization by Evaluation for Non-cumulativity | ICFP 2025 | 2025-10-12 |
Claims that untyped NbE for non-cumulativity is sound and complete for a Martin-Löf style type theory with explicit universe levels, gives a mechanized proof… | ||
| McTT: A Verified Kernel for a Proof Assistant | ICFP 2025 | 2025-10-12 |
A fully verified kernel for core Martin‑Löf type theory is implemented in Rocq, proving normalization, consistency and injectivity of constructors and proving… | ||
| McTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory | WITS 2025 | 2025-01-25 |
A correct-by-construction Coq implementation of Martin-Löf type theory produces an end-to-end proof checker, with formalized cumulative universe hierarchy and… | ||
| A Dependent Type Theory for Meta-programming with Intensional Analysis | POPL 2025 | 2025-01-19 |
Introduces DeLaM, a concrete dependent layered modal type theory that implements three layers (syntax, MLTT, meta) with quoting of open code, composition… | ||
| nothing matches | ||